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