remotely deleting a branch

From: jean-luc malet <jeanluc.malet@gmail.com>
Date: Jun 1, 2009, 10:16 UTC
Message-ID: <1de9d39c0906010316v657f2624i3f16b8b5bea73122@mail.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? thanks JLM

-- 
KISS! (Keep It Simple, Stupid!)
(garde le simple, imbécile!)
"mais qu'est-ce que tu m'as pondu comme usine à gaz? fait des choses
simples et qui marchent, espèce d'imbécile!"
-----------------------------
"Si vous pensez que vous êtes trop petit pour changer quoique ce soit,
essayez donc de dormir avec un moustique dans votre chambre." Betty
Reese
http://www.grainesdechangement.com/citations.htm