Stream: Miscellaneous

Topic: Gitter Features on Zulip

view this post on Zulip Jason Gross (May 31 2020 at 23:38):

I liked the feature where hovering over a link to a Coq PR would display a popup with the title and description of that PR. Can we get that feature back on Zulip?

view this post on Zulip Gaëtan Gilbert (Jun 05 2020 at 21:22):

The notifications are more readable on gitter. The most noticeable difference is that they're far less verbose as they only say "User did Event on #XXXX" where zulip posts the entire message. Can we cnahge that?

view this post on Zulip Théo Zimmermann (Jun 06 2020 at 16:52):

It's a plugin, and it is probably open source, so one could try to improve it. @Cyril Cohen might know more.

Last updated: May 24 2024 at 23:01 UTC