git issue on windows

Stream: general

[Sebastien Gouezel]

Trying to fetch from github, I get the issue

error: cannot lock ref 'refs/remotes/origin/NCard->Card': Unable to create 'C:/Users/Sebastien/Desktop/mathlib4_2/.git/refs/remotes/origin/NCard->Card.lock': Invalid argument

My guess is that the filename NCard->Card.lock is forbidden on windows. @apnelson1, would you agree to rename your branch to something more standard?

[Rémy Degenne]

@Peter Nelson

[Eric Wieser]

Does the error cancel fetching the other refs, or does it just drop that one?

[Peter Nelson]

Sorry! I’ll fix this as soon as I get to a computer (10 mins)

[Sebastien Gouezel]

Eric Wieser said:

Does the error cancel fetching the other refs, or does it just drop that one?

git stops on this error, so git pull is not working for me.

[Eric Wieser]

I would guess git pull origin master might be ok as a workaround

[Eric Wieser]

This answer on SO suggests that enabling reftable might teach windows to handle these paths, but I suspect it's experimental and certainly we should just avoid having branches with these names!

[Peter Nelson]

Ok, I've deleted the branch entirely (it seemed that just renaming it left remnants of the old name in the system). Sorry again about this!

[Sebastien Gouezel]

Thanks! It looks like the bad character is >.