mathlib3
3c2bc2e7 - lint(scripts/lint-style.py): add indentation linter (#10257)

Commit

4 years ago

lint(scripts/lint-style.py): add indentation linter (#10257)

Author

jcommelin

jcommelin

Parents

Loading