Kevin Kappelmann (Sep 22 2019 at 15:07): 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?
Kevin Kappelmann (Sep 22 2019 at 16:31):@Anthony Bordg just figured out that you are the/an admin :)
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.
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!
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:
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 21 2024 at 12:33 UTC