Def lintAllFiles

Modification history

2024-07-13 13:40

Mathlib/Tactic/Linter/TextBased.lean

refactor: improvements to lint_style (#14676) …

Deleted lintAllFiles View on Github →

2024-06-23 07:52

Mathlib/Tactic/Linter/TextBased.lean

feat(lint-style): fix `update-style-exceptions.py`; produce human-readable output by default (#14012) …

Modified lintAllFiles View on Github →

2024-06-21 07:01

Mathlib/Tactic/Linter/TextBased.lean

feat: rewrite file length check in Lean (#13620) …

Added lintAllFiles View on Github →