two branches differing only through capitalization

Stream: mathlib4

[Sébastien Gouëzel]

@Anne Baanen , you are owning two different branches integrallyClosedIn and IntegrallyClosedIn. Windows doesn't like that, unfortunately. Could you delete or rename one of them?

[Junyan Xu]

On the other hand, Mac doesn't like checking out a branch where a file name's capitalization is changed ... many times I had to delete the file before checkout, but I later find out I can force checkout.

[Anne Baanen]

Oops! integrallyClosedIn is the correct one. GitHub UI doesn't even display the IntegrallyClosedIn branch so I had to try and remember which magic commands delete it on the server - did I do it right?

[Sébastien Gouëzel]

Perfect, thanks!