deleting branches

[Herbert Valerio Riedel]

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