This should of course have been cc to the list too...
Gustaf Hendeby wrote:
jean-luc malet wrote:
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?
thanks
JLM
Hi Jean-Luc!
Have a look at the help for push, you will find
git push origin :mynewbranch
to be what you are looking for. It is listed quite far down as an example.
/Gustaf
--
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html