Commit 2024-09-30 12:08 dfc92350
View on Github →chore(Tactic/Linter): do not import TextBased linter (#17187)
Mathlib.Tactic.Linter.TextBased is only used by the script lake exe lint-style and therefore does not to be imported by Mathlib.
chore(Tactic/Linter): do not import TextBased linter (#17187)
Mathlib.Tactic.Linter.TextBased is only used by the script lake exe lint-style and therefore does not to be imported by Mathlib.