Zulip Chat Archive

Stream: new members

Topic: mathlib PR

Bernd Losert (Jan 16 2022 at 15:31):

I made a PR to mathlib (https://github.com/leanprover-community/mathlib/pull/11445), but the PR is in a fork. I was told that I should make a branch instead, but I can't push the branch without the required permission. Can someone grant me the required permissions please?

My github username is berndlosert.

Patrick Massot (Jan 16 2022 at 16:06):

Done. Sorry I should have checked whether you were already in.

Bernd Losert (Jan 16 2022 at 16:15):


Last updated: Dec 20 2023 at 11:08 UTC