Weird git behavior

Stream: mathlib4

[Sebastien Gouezel]

Whenever I pull from mathlib4, I get the message

PS C:\Users\Sebastien\Desktop\mathlib4_2> git pull
From https://github.com/leanprover-community/mathlib4
 * [new branch]            ClausenCl/UniformDistribution -> origin/ClausenCl/UniformDistribution
Already up to date.

(So if I pull three times in a row I get three times this message). Is there something fishy with this branch?

[Sebastien Gouezel]

(And it appears twice on the branch list on github)

[Sebastien Gouezel]

I think I get it: there are two branches ClausenCl/UniformDistribution and ClausenCl/Uniformdistribution, with D and d respectively. On some filesystems, it has to create some confusion. Could we delete one of the two branches? @Claus Clausen

[Eric Wieser]

Another option (on Windows) is maybe to run

fsutil.exe file setCaseSensitiveInfo path/to/mathlib enable

as an administrator

[Oliver Nash]

I just encountered this issue now. I think Sebtastian's suggestion is the way to go since it should fix the issue for all users. I find it rather strange that is has not surfaced before: neither branch has had any commits added for two days.

[Oliver Nash]

image.png
@Claus Clausen Can one of these branches be safely deleted?

[Eric Wieser]

We had exactly this problem before with a previous branch of Kevin's

[Floris van Doorn]

I went ahead and deleted branch#ClausenCl/UniformDistribution, since the other one is the same, but with 3 more commits.

[Claus Clausen]

Oliver Nash schrieb:

image.png
Claus Clausen Can one of these branches be safely deleted?

Yes sorry, I had some trouble with my commits. I thought closing it would be sufficient! Sorry for the trouble and thank you @Floris van Doorn for your quick thinking!