CI label

Stream: mathlib4

[Michael Rothgang]

Does the CI label also cover PRs adding or modifying lints? If so, could the label description be changed?

[Michael Rothgang]

To un-#xy: I've noticed that PRs adding or tweaking lints don't have a natural label. Is that a small thing worth changing?

[Michael Rothgang]

Broader motivation: should each PR have a topic label? Because e.g. lint changes don't have a natural label right now.

[Michael Rothgang]

Perhaps this is not important; that's also fine. It's a small papercut I noticed.