Note the colon before the name... that is what causes the remote
branch to be deleted. My understanding is that you are literally
pushing a void local branch over the remote branch, which effectively
deletes it.
Since Git 1.7, I believe you can also:
git push origin --delete origin/wip/new-flatten-skolems-Aug14
which is just sugar for what Herbert said.
On Wed, Sep 10, 2014 at 11:00 AM, 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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs