Stream: Coq devs & plugin devs

Topic: stream events


view this post on Zulip Notification Bot (May 07 2020 at 09:03):

Théo Zimmermann renamed stream coq to Coq and plugin development.

view this post on Zulip Théo Zimmermann (May 07 2020 at 09:17):

I've renamed this channel to better reflect its more common use case (from the Gitter times) and I was thinking about creating a new "Beginners" or "New members" stream (to highlight that basic questions are welcome). But this can probably wait a bit, especially given that anyone can create a new stream, not just admins.

view this post on Zulip Notification Bot (May 08 2020 at 11:14):

Théo Zimmermann renamed stream Coq and plugin development to Coq devs & plugin devs.

view this post on Zulip Notification Bot (Apr 13 2022 at 09:47):

Théo Zimmermann changed the access permissions for this stream from Public, protected history to Web-public.

view this post on Zulip Gaëtan Gilbert (Apr 13 2022 at 09:50):

what's "protected history" about?

view this post on Zulip Théo Zimmermann (Apr 13 2022 at 09:51):

Dunno. Protected history is supposed to be for private streams, not for public ones. Maybe they encode this with a boolean and it is displayed even when irrelevant.

view this post on Zulip Théo Zimmermann (Apr 13 2022 at 09:51):

Note that when I did the same change on the #Announcements stream, it didn't say "protected history".

view this post on Zulip Théo Zimmermann (Apr 13 2022 at 09:51):

Should we report this confusing message to Zulip's bug tracker?

view this post on Zulip Gaëtan Gilbert (Apr 13 2022 at 09:54):

why not

view this post on Zulip Théo Zimmermann (Apr 13 2022 at 11:44):

https://github.com/zulip/zulip/issues/21784


Last updated: Feb 05 2023 at 21:03 UTC