Zulip Chat Archive

Stream: Zulip meta

Topic: name of this stream

Johan Commelin (Apr 29 2020 at 14:19):

should this stream be called "zulip meta"? I first thought that this was about interacting with lean in server mode...

Jalex Stark (Apr 29 2020 at 14:25):

I think changing stream names is an admin privelege

Jalex Stark (Apr 29 2020 at 14:28):

Is there a mapping user -> role that's visible by clicking on buttons in the zulip UI?

Johan Commelin (Apr 29 2020 at 14:29):

Yes, in Settings, go to Users, and sort by Role

Johan Commelin (Apr 29 2020 at 14:29):

You will find Mario and Sebastian

Jalex Stark (Apr 29 2020 at 15:25):

Comment: "'zulip meta' meta" meta
The name of this topic should be "'zulip meta' meta"

Last updated: Dec 20 2023 at 11:08 UTC