Def Mathlib.Linter.TextBased.modulesOSForbidden

Modification history

2025-12-05 11:03
Mathlib/Tactic/Linter/TextBased.lean
chore(Tactic/Linters): remove `public section` (#31803) …
Deleted Mathlib.Linter.TextBased.modulesOSForbiddenView on Github →
2025-09-15 10:13
Mathlib/Tactic/Linter/TextBased.lean
feat: verify that file names contain no forbidden characters (#27965) …
Added Mathlib.Linter.TextBased.modulesOSForbiddenView on Github →