Zulip Chat Archive
Stream: maths
Topic: category_theory/groupoid and category_theory/Groupoid
Chris Hughes (Aug 22 2019 at 06:09):
The files category_theory/groupoid and 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: Dec 20 2023 at 11:08 UTC