github

Stream: general

[Scott Morrison]

What am I meant to do with old PRs, that I had pushed as branches on leanprover-community/mathlib?

[Scott Morrison]

It seems I can no longer push to them, which is probably an intentional effect of the new maintainer setup.

[Scott Morrison]

Should I close those PRs and make new ones from my own fork?

[Kenny Lau]

I believe you should change the remote to the fork and push them there

[Scott Morrison]

I should I still be able to push to non-master branches?

[Kenny Lau]

And for the new PR's you can push them to the non-master branches

[Scott Morrison]

I'm confused. Are you saying that I can make new branches on leanprover-community/mathlib, but can't push to old branches?

[Kenny Lau]

I'm saying that for old PR's, you can change the remote to the backup fork and push them there (if you push without changing remote, you'll create a new branch in leanprover-community/mathlib); for new PR's push to leanprover-community/mathlib directly

[Simon Hudon]

I second @Kenny Lau's suggestion

[Scott Morrison]

It seems I can't push to leanprover-community/mathlib anymore?

[Kenny Lau]

you should be able to...

[Scott Morrison]

I'd missed the invitation. All good now.