From: John Tapsell <johnflux@gmail.com>
Date: Mon, 01 Jun 2009 11:02:23 GMT
Subject: Re: remotely deleting a branch
Message-ID: <43d8ce650906010402t792df314v1ed632e79f42bca7@mail.gmail.com>
In-Reply-To: <1de9d39c0906010316v657f2624i3f16b8b5bea73122@mail.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