Olá a todos!
Percebi agora que todas as menções ficam cinzas, então a menção de um usuário pode passar despercebida se estiver em uma lista grande de menções (às vezes acontece):
Seria muito conveniente ter a própria menção colorida de forma diferente, como no Slack:
Existe alguma solução, ou estou perdendo algo? Obrigado!
O usuário mencionado (como esperado) recebe uma notificação de qualquer maneira, para que possa ver se foi mencionado. Eu nunca perdi uma notificação de menção.
Os usuários também podem ver todas as suas menções aqui
https://your.discoursesite-name/my/notifications/mentions
Obrigado, @ondrej! Tudo parece razoável, mas tive uma situação outro dia em que um usuário não percebeu que foi mencionado, pois seu nome de usuário era “user99999” 
Provavelmente é um caso bem raro, mas ainda assim, seria bom ter o nome de usuário de alguém se destacando em uma postagem.
