Commit 2020-07-29 11:45 37e13a01

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