Commit 2024-09-01 23:38 3bea0ec4

View on Github →

chore: remove the text-based long file linter (#16299) It is superseded by the longFile syntax linter now.

Estimated changes

Modified Mathlib/Tactic/Linter/TextBased.lean

modified def Mathlib.Linter.TextBased.StyleError.errorMessage

deleted def Mathlib.Linter.TextBased.allLinters

modified def Mathlib.Linter.TextBased.lintFile

Modified scripts/lint-style.py

Modified scripts/technical-debt-metrics.sh