Allow ignoring mentions from a specific user

[tgr]

Your use case

Certain bots generate uninformative mentions (e.g. a repo notifaction bot generates a message if I push a commit to the repo, and that message will contain my username). Mentions are noisy (result in phone buzz) so I'd like to prevent them.

Similar to the "Ignore" option in the member details panel, there should be something like "Ignore mentions".

Have you considered any alternatives?

• Use existing ignore option: hides all messages from the given user/bot. I still want to see their messages (e.g. to know when other users push to the repo), just don't want my phone buzzed and my OS send popups every time .
• Silence the room: it's used by other bots and humans, some of whose messages to me are important.

Additional context

No response