[coldtea]

>The point of the "grammar nazi" bots is to focus on the actual problems: if a bot is deciding about linting, you don't have to waste brain power to discuss it in PRs.

And yet, as per the example, the bot force worse linting decisions, and even pushes towards more bugs (e.g. future readers missing the comment intention since it now applies to all 3).

[mrbombastic]

the claim we are arguing here is not that “linters never make mistakes” it is that “linters are generally beneficial and avoid mostly useless debates we previously spent an inordinate amount of time on” Most linters have an escape hatch for exactly this which is usually a one line disable comment