Hi, Edvard!
I renamed the local directory after cloning. If Git really cannot deal with this, then this is yet another reason for preferring darcs over Git.
Unfortunately, it would be hard to reproduce this problem, since I took slightly different steps before incorporating the linear-types branch, as I did not yet know about the documentation on getting the linear-types branch at that time.
All the best,
Wolfgang
Am Montag, den 10.07.2017, 11:22 +0200 schrieb Edvard Hübinette:
Hi Wolfgang,
the directory name should not matter (mine is named differently for example). Renaming the base directory after cloning (instead of using git clone foo dir-name) can sometimes confuse git, if that might be the problem.
In any case, we are unable to reproduce this so if you could provide exact reproductions steps we can update the guide. Your git version may be useful as well.
Cheers,
Edvard