Zulip Chat Archive
Stream: mathlib4
Topic: github access
Richard Osborn (Nov 25 2022 at 20:06):
Hi, I would like to start contributing to the mathlib port. Could I get permission to push branches to the repo? Thanks!
Scott Morrison (Nov 25 2022 at 21:45):
What is your github username?
Richard Osborn (Nov 25 2022 at 21:48):
My username is rosborn.
Richard Osborn (Nov 25 2022 at 21:55):
Do I also need access to mathlib to edit the port status wiki?
Last updated: Dec 20 2023 at 11:08 UTC