deleting branches

2014-09-10 Thread Simon Peyton Jones
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

Re: deleting branches

2014-09-10 Thread 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