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?
@Anthony Bordg just figured out that you are the/an admin :)
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.
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!
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:
Here you can find the first working version of the archive. The repo is here
Last updated: Dec 07 2024 at 16:22 UTC