Zulip Chat Archive

Stream: Zulip meta

Topic: name of this stream


view this post on Zulip 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...

view this post on Zulip Jalex Stark (Apr 29 2020 at 14:25):

I think changing stream names is an admin privelege

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:29):

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

view this post on Zulip Johan Commelin (Apr 29 2020 at 14:29):

You will find Mario and Sebastian

view this post on Zulip 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: May 08 2021 at 21:09 UTC