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