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
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
