Def lintStyleCli

Modification history

2024-06-24 11:40

Mathlib/Tactic/Linter/TextBased.lean

chore: move `lint_style` executable to the `scripts` directory (#14057) …

Modified lintStyleCli 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) …

Added lintStyleCli View on Github →