Re: remotely deleting a branch

[John Tapsell <johnflux@gmail.com>]

2009/6/1 jean-luc malet <jeanluc.malet@gmail.com>:
> hi!
> I created a remote branch by doing
> $ git push origin mynewbranch
> I done some work on mynewbranch, commited, pushed changes to origin,
> merged it to master and pushed to origin and deleted the mynewbranch
> localy because I don't need it anymore
> now I want to "undo" the git push origin mynewbranch ie remotely
> delete the branch from the repository
> I tried git push --mirror but it deleted all remote branches that I
> didn't worked on... I don't want to have it be a mirror... but
> something like
> $ git branch -r -d origin/mynewbranch
> $ git push
>   ---> deleting origin/mynewbranch
>
> how shall I do that?

Yeah, it's pretty confusing on how to delete a remote branch.  The
magic command is:

git push origin -f :mynewbranch

Hopefully someone will figure out a way to make git a bit more
intuitive in this respect.  Maybe a remote option for git branch -d or
something.
John