Zulip Chat Archive
Stream: new members
Topic: non master branch access
Eric (Jul 04 2022 at 08:25):
Hello! I am Eric. My github username is ericluap. Am asking for non-master branch access for PR #15110.
Just started learning lean! I look forward to learning more and improving.
Eric Wieser (Jul 04 2022 at 08:27):
Hi Eric, I just granted you access!
Eric (Jul 04 2022 at 08:28):
wonderful, thank you!
Last updated: May 02 2025 at 03:31 UTC