Zulip Chat Archive

Stream: new members

Topic: permission for mzinkevi to push to github

Martin Zinkevich (Sep 19 2020 at 01:20):

github username: mzinkevi

In watching https://www.youtube.com/watch?v=Bnc8w9lxe8A
Scott Morrisson suggests to ask for permission to push to github in Zulip.

My long-term goal is to add the Radon-Nikodym from
in small chunks, but first I need to create a branch on github to create a pull request, which requires permission.


Bryan Gin-ge Chen (Sep 19 2020 at 01:23):

@Martin Zinkevich Invitation sent! https://github.com/leanprover-community/mathlib/invitations

Martin Zinkevich (Sep 19 2020 at 02:38):

Thanks! I successfully created my first PR https://github.com/leanprover-community/mathlib/pull/4184

Last updated: Dec 20 2023 at 11:08 UTC