On 2014-09-10 at 11:53:05 +0200, Simon Peyton Jones wrote: > 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 Here's the problem: you are not allowed to delete anything outside the "wip/" namespace (partly because we don't want you do delete a branch like "ghc-7.8" or "master", and partly because the submodule gitlink integrity check assumes that all branches outside "wip/" are to exist forever) however, here's how you'd usually delete that *remote* branch, if you were allowed to (and what I've just done for you, as I have the necessary perms being an Git admin): git push origin :origin/wip/new-flatten-skolems-Aug14 'git branch -D' deletes only your local branches In the future, we will restrict the ability to create new branches outside the "wip/" namespace to avoid such mistakes _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
