Running the linter locally

Stream: new members

[Frédéric Dupuis]

Is there a way to run the linter locally to make sure all the checks pass before committing?

[Jalex Stark]

#lint

[Jalex Stark]

i usually put it at the bottom of the file but maybe one can put it anywhere instead

[Floris van Doorn]

To elaborate on Jalex: #lint checks all declarations in that file (above the #lint command). There is also #lint_mathlib that checks in all files (in mathlib) that you've imported.

[Frédéric Dupuis]

Thanks!