Def checkFileLength
Modification history
2024-08-27 23:34
Mathlib/Tactic/Linter/TextBased.lean
chore(Linter/TextBased): namespace declarations (#16203) …
Deleted checkFileLengthView on Github →2024-08-09 00:58
Mathlib/Tactic/Linter/TextBased.lean
refactor: polish `lint_style` and rename to lint-style (#14757) …
Modified checkFileLengthView on Github →2024-07-29 01:34
Mathlib/Tactic/Linter/TextBased.lean
fix: re-add the `TextBased` long line linter (#15190) …
Added checkFileLengthView on Github →2024-07-25 22:15
Mathlib/Tactic/Linter/TextBased.lean
feat: the long line linter as a syntax linter (#15097) …
Deleted checkFileLengthView on Github →2024-06-25 01:47
Mathlib/Tactic/Linter/TextBased.lean
feat: rewrite line length style linter in Lean (#14093) …
Added checkFileLengthView on Github →