Zulip Chat Archive

Stream: maths

Topic: category_theory/groupoid and category_theory/Groupoid


view this post on Zulip 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.

view this post on Zulip Chris Hughes (Aug 22 2019 at 06:52):

#1353

view this post on Zulip Wojciech Nawrocki (Aug 22 2019 at 19:31):

This didn't cause problems on windows? It's also case-insensitive

view this post on Zulip Chris Hughes (Aug 22 2019 at 20:09):

Did you ever checkout that commit? It was only like that for half a day.

view this post on Zulip 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