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