Linting all of mathlib locally

Stream: general

[Yakov Pechersky]

I am trying to create an all.lean so that I can run linters locally. leanproject mk-all seems to be a no-op. (the file is src/all.lean, but not made if src/all.lean exists, iiuc). What's the right approach here?

[Floris van Doorn]

run scripts/mk_all.sh