Mentionning a Discord user from IRC does not work

[JulienPalard]

We tried login: ..., @login: ..., @login#id: ..., nothing triggers an HL discord side, any idea how it could be implemented?

[debnet]

It's possible to ping a Discord user from IRC by using a dedicated format: <@user_id>.

The Discord user ID is internal to Discord but can be obtained by right-clicking the user:

It doesn't help much though.

[Hackndo]

I guess it could be implemented by looping through all users on a discord channel and getting the right ID and then using it. I don't intend to implement it, but you can PR if this is something needed. I'll let this issue open, if someone wants it implemented.