deleting branches

Simon Peyton Jones simonpj at microsoft.com
Wed Sep 10 09:53:05 UTC 2014


I accidentally created a branch (in the main repo) called
               origin/origin/wip/new-flatten-skolems-Aug14
I was trying to make a local branch to track the existing origin/wip/new-flatten-skolems-Aug14, but only succeeded in creating a local branch called origin/wip/new-flatten-skolems-Aug14, which I then pushed, creating the one above.
It's quite confusing to me that branches (listed with git branch -av) have names like
               wip/rae
and
               remotes/origin/wip/rae
I suspect that the "remotes/origin" part isn't really part of the name of the branch at all, even though it is not syntactically distinguished.
Anyway, I'd like to delete that branch from the main repo on the server, but I don't know how to do so.  I tried

git branch -D origin/origin/wip/new-flatten-skolems-Aug14

error: branch 'origin/origin/wip/new-flatten-skolems-Aug14' not found.
My model of branch naming is not working well.  Can anyone advise?
Simon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140910/480e3d01/attachment.html>


More information about the ghc-devs mailing list