Zulip Chat Archive
Stream: new members
Topic: Add to mathlib
Andre Hernandez-Espiet (Rutgers) (Sep 14 2022 at 17:23):
Can someone please let me know what permissions are needed to be able to PR to mathlib?
Ruben Van de Velde (Sep 14 2022 at 17:25):
You ask the @maintainers here and you get an invite :)
Kyle Miller (Sep 14 2022 at 17:27):
@Andre Hernandez-Espiet (Rutgers) What's your github username?
Andre Hernandez-Espiet (Rutgers) (Sep 14 2022 at 17:42):
ah1112
Kyle Miller (Sep 14 2022 at 17:48):
@Andre Hernandez-Espiet (Rutgers) Invite sent!
Last updated: Dec 20 2023 at 11:08 UTC