Stream: Coq devs & plugin devs

Topic: Github Notifications

view this post on Zulip Notification Bot (May 21 2020 at 20:15):

This topic was moved by Théo Zimmermann to #GitHub notifications > Coq Notifications

view this post on Zulip Théo Zimmermann (May 21 2020 at 20:18):

I've moved the three notification topics to a specific stream to answer the request of @Emilio Jesús Gallego Arias at coq/coq#12382. Let's see what this gives.

view this post on Zulip Emilio Jesús Gallego Arias (May 21 2020 at 22:16):

Thanks a lot folks; maybe I'm alone in my use case but I tend to click on streams, and use the "new messages" info so I was getting a bit of noise in that sense.

Last updated: Sep 15 2024 at 13:02 UTC