Hello all,

I first want to point out that git's way of deleting a remote branch is "sane", since their syntax is:

git push <remote> <localbranch>:<remotebranch>

so doing "git push origin :mycrazyfeature" means "push on origin at remote branch mycrazyfeature the empty local branch", which means "delete mycrazyfeature branch".

They later added (I think in 1.7.0) the option to delete a branch even in a more intuitive fashion:

git push <remote> --delete <remotebranch>

However, I think all this sort of "problems" we are having could be just fixed with the pushkey idea (http://mercurial.selenic.com/wiki/PushkeyConcept).

On the remote, an extension can be enabled to understand certain commands, meaning that we could drop a named branch or even an anonymous branch. A fast idea that comes to mind is performing an "hg clone -r ..." with all the wanted branches, leaving those that aren't of interest. Your old clone on the remote would become deleted, and the new one renamed to have the same name as the old repository.

This would be capable (being run on the remote) of removing all kind of branches (named and unnamed), having a very similar git behavior. We have to take into account the "genie is out of the bottle" problem, but in theory this is going to be done in personal repositories before they get merged upstream, so I believe this is not a problem.

Comments ?