Zulip Chat Archive
Stream: mathlib4
Topic: Override folder naming in mathport
Moritz Doll (May 21 2023 at 22:24):
We have now the folder Analysis.Calculus.FDeriv.foo, but in mathport it gets named to Analysis.Calculus.Fderiv.foo, is there a way to re-align this?
Last updated: Dec 20 2023 at 11:08 UTC