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.

[JulienPalard]

We fixed something about that in https://git.afpy.org/AFPy/discord-irc-sync/commit/bba218ea8c5b6e86bc69a2777ae5c88808accbc2, we're currently testing it.

We had to fix, using: https://git.afpy.org/AFPy/discord-irc-sync/commit/403fa4f512e9eb346fe7e54a0d9f7a0c1b47fc27

Looks like it works.