Théo Zimmermann renamed stream coq to Coq and plugin development.
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.
Théo Zimmermann renamed stream Coq and plugin development to Coq devs & plugin devs.
Théo Zimmermann changed the access permissions for this stream from Public, protected history to Web-public.
what's "protected history" about?
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.
Note that when I did the same change on the #Announcements stream, it didn't say "protected history".
Should we report this confusing message to Zulip's bug tracker?
Last updated: Dec 07 2023 at 06:38 UTC