disable "Note: This linter can be disabled with ..."?

Stream: lean4

[Malvin Gattinger]

When reading a long list of linter output I found it noisy to have this linke repeated each time. With many linter warnings after each other I also get confused whether the Note: ... line belongs to the warning just above or just below it. I also think that in many cases the reader of these messages might not be "supposed to" disable the warning anyway (e.g. when working in Mathlib).

So it would be nice to have an option to turn off the Note line completely. Or is there some way to do that already?

[Kenny Lau]

why are you triggering so many linters?

[Malvin Gattinger]

I have a project where I only turned them on today, so there were quite many things to fix :innocent:

[Kevin Buzzard]

Oh yeah I remember that phase! I turned them on one at a time and made liberal use of the various ways to mark exceptions so I didn't get overwhelmed, ie I had some JSON file saying "actually don't lint this" and then went through it slowly fixing the problems.