Def toLeanOptions

Modification history

2025-05-19 09:39
scripts/lint-style.lean
feat(scripts/lint-style): select linters with Lakefile options (#24953) …
Added toLeanOptionsView on Github →