Zulip Chat Archive

Stream: general

Topic: oops!

Scott Morrison (Oct 26 2019 at 07:37):

errr... I just pushed directly to lean-3.4.2 by accident.

Scott Morrison (Oct 26 2019 at 07:37):

I guess I should force push to undo??

Scott Morrison (Oct 26 2019 at 07:39):

Crap, I can't. When I git reset HEAD~1 and git push --force, githup tells me I can't force push to a protected branch. So how did it let me push to that branch in the first place?

Scott Morrison (Oct 26 2019 at 07:41):

The evil commit is now an honest PR, at https://github.com/leanprover-community/mathlib/pull/1616. Maybe we can just merge that quickly. :-)

Simon Hudon (Oct 26 2019 at 07:43):

It looks good to me

Simon Hudon (Oct 26 2019 at 07:43):

The branch protection is weaker than I expected. I made a similar mistake recently

Simon Hudon (Oct 26 2019 at 07:44):

What I did is temporarily disable the branch protection (by changing the master filter with master-) so that I can backpedal. But if this is ready to merge, I can just merge it

Mario Carneiro (Oct 26 2019 at 07:45):

wrong branch

Simon Hudon (Oct 26 2019 at 07:46):

That was the branch I had an issue with. The same idea works with other branch protection rules (details left as an exercise)

Scott Morrison (Oct 26 2019 at 07:47):

Let's let travis finish, but as this is just a "move proofs about" PR, it should be safe to merge immediately afterwards.

Mario Carneiro (Oct 26 2019 at 07:47):

I reverted it

Mario Carneiro (Oct 26 2019 at 07:48):

I think travis should still run to completion

Last updated: Dec 20 2023 at 11:08 UTC