Fine-tuning notifications

Stream: mathlib4

[Yaël Dillies]

I notice I receive too many notifications of some kind and too few of others. I would like to know what's the experience for other people. Here are two examples:

• When I write maintainer merge, I always receive a notification about the automatic message sent by github-actions to say I put the PR on the merge queue. See eg here. I don't think we really need this message. Adding the maintainer-merge label would be enough to signify that the maintainer merge command was picked up, and wouldn't send me a useless notification.
• What often happens when you review a PR is that you get a notification when the PR author changes something, but CI isn't done yet so you are not sure whether you should be looking. It's not uncommon that a PR drops off my radar this way. This would be fixed if I was given a notification every time a PR is back on #queue.