Zulip Chat Archive

Stream: general

Topic: testing in production


Johan Commelin (Sep 19 2022 at 17:51):

As you may have noticed, I merged a testing PR into mathlib master by accident. Sorry! I have already reverted the commit.

But things got worse: I disabled a bunch of CI workflows on leanprover-community/mathlib. Again, I thought I was working on my own testing copy :face_palm: I'm really sorry if this canceled CI on your branch.

By now, everything should be back in good state.


Last updated: Dec 20 2023 at 11:08 UTC