mathlib3
7b7cd0a1 - fix(tactic/lint): punctuation of messages (#7869)

Commit
4 years ago
fix(tactic/lint): punctuation of messages (#7869) Previously, the linter framework would append punctuation (`.` or `:`) to the message provided by the linter, but this was confusing and lead to some double punctuation. Now all linters specify their own punctuation. Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
Author
Parents
Loading