mathlib
37e13a01 - feat(tactic/lint): quieter output by default (#3622)

Commit
5 years ago
feat(tactic/lint): quieter output by default (#3622) * The behavior of `lint-` hasn't changed. * `lint` will now suppress the output of successful checks. If everything succeeds, it will print "All linting checks passed!" * `lint+` behaves like the old `lint`. It prints a confirmation for each test. Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/quiet.20linter Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Author
Parents
Loading