Chris Hughes (Aug 22 2019 at 06:09):
category_theory/Groupoid differ by the case of one character. This is apparently a problem on older macs, which are case insensitive. I guess this needs to be changed.
Chris Hughes (Aug 22 2019 at 06:52):
Wojciech Nawrocki (Aug 22 2019 at 19:31):
This didn't cause problems on windows? It's also case-insensitive
Chris Hughes (Aug 22 2019 at 20:09):
Did you ever checkout that commit? It was only like that for half a day.
Wojciech Nawrocki (Aug 23 2019 at 12:46):
Oh no, I was just wondering where else it could be problematic.
Last updated: May 11 2021 at 16:22 UTC