Def toLeanOptions

Modification history

2025-10-13 06:34
scripts/lint-style.lean
fix(lint-style): parse linter options and load environment extensions correctly (#29513) …
Modified toLeanOptionsView on Github →
2025-05-19 09:39
scripts/lint-style.lean
feat(scripts/lint-style): select linters with Lakefile options (#24953) …
Added toLeanOptionsView on Github →