Commit 2025-07-29 02:51 713ead03

View on Github →

feat(Linter/TextBased): linter against Windows-forbidden filenames (#27588) Zulip

Estimated changes

Modified Mathlib/Tactic/Linter/TextBased.lean

added def Mathlib.Linter.TextBased.modulesForbiddenWindows

Created MathlibTest/ForbiddenWindows.lean

added def testModulesForbiddenWindows

Modified scripts/lint-style.lean