lean/scripts/lint_style.py (1 line):
	- line 127: # TODO: some string literals (in e.g. tactic output messages) can be excepted from this rule