Stream: General

Topic: Zulip archive


view this post on Zulip Kevin Kappelmann (Sep 22 2019 at 15:07):

I wanted to create a Zulip archive (just like the Lean folks are doing it). The script is available on github. For this, I need to add a bot to the Isabelle Zulip group, but I do not have permissions to do so. Can someone please grant me admin rights so I can set this up?

view this post on Zulip Kevin Kappelmann (Sep 22 2019 at 16:31):

@Anthony Bordg just figured out that you are the/an admin :)

view this post on Zulip Anthony Bordg (Sep 22 2019 at 16:50):

I wanted to create a Zulip archive (just like the Lean folks are doing it). The script is available on github. For this, I need to add a bot to the Isabelle Zulip group, but I do not have permissions to do so. Can someone please grant me admin rights so I can set this up?

This is an excellent idea. According to the current settings, admins and members can add bots.

view this post on Zulip Kevin Kappelmann (Sep 22 2019 at 19:40):

I wanted to create a Zulip archive (just like the Lean folks are doing it). The script is available on github. For this, I need to add a bot to the Isabelle Zulip group, but I do not have permissions to do so. Can someone please grant me admin rights so I can set this up?

This is an excellent idea. According to the current settings, admins and members can add bots.

Cool, will add it tomorrow!

view this post on Zulip Kevin Kappelmann (Sep 22 2019 at 19:48):

FYI, I also requested Zulip Standard for the Isabelle Zulip group, which was now granted for free thanks to Zulip supporting open-source communities :party_ball:

view this post on Zulip Kevin Kappelmann (Sep 23 2019 at 23:07):

Here you can find the first working version of the archive. The repo is here


Last updated: Dec 07 2024 at 16:22 UTC