mathlib

e5bd9413 - feat(scripts): make style lint script more robust to lines starting with spaces (#13317)

feat(scripts): make style lint script more robust to lines starting with spaces (#13317) Currently some banned commands aren't caught if the line is indented. Because of this I previously snuck in a `set_option pp.all true` by accident