Commit 2024-07-29 01:34 e670f867

fix: re-add the TextBased long line linter (#15190) As pointed out on Zulip, the TextBased long line linter should not have been removed. There are two advantages to having also the TextBased linter:

• if you accidentally submit code with long lines, the TextBased linter will tell you of all long lines at once;
• the linter can only flag lines on files that import the linter, while the TextBased linter crawls all .lean files in Mathlib.