Def getLakefileLeanOptions

Modification history

2025-05-19 09:39

scripts/lint-style.lean

feat(scripts/lint-style): select linters with Lakefile options (#24953) …

Added getLakefileLeanOptions View on Github →