Def lintStyle

Modification history

2024-08-09 00:58
scripts/lint-style.lean
refactor: polish `lint_style` and rename to lint-style (#14757) …
Added lintStyleView on Github →