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
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