Zulip Chat Archive
Stream: new members
Topic: Permission to push branch
Bart Michels (Jun 11 2022 at 14:50):
Hi, I've been practicing lean for a little while and have a few things to make a PR to mathlib. Could I get permission to push a branch? My username is bartmichels
Last updated: Dec 20 2023 at 11:08 UTC