mathlib3
7bf0850d - fix(scripts): Allow special character in file names (#11001)

Commit

2 years ago

fix(scripts): Allow special character in file names (#11001) We don't have any files like this in mathlib, but it probably doesn't hurt to be safe here.

Author

eric-wieser

Parents

5c4b3d41

mathlib3 7bf0850d - fix(scripts): Allow special character in file names (#11001)

mathlib3
7bf0850d - fix(scripts): Allow special character in file names (#11001)