Zulip Chat Archive
Stream: mathlib4
Topic: CI
Yury G. Kudryashov (Jun 07 2023 at 17:44):
On !4#4814, CI didn't run any tests.
Yury G. Kudryashov (Jun 07 2023 at 17:45):
UPD: ignore, it's already in No, wrong branchmaster
Yury G. Kudryashov (Jun 07 2023 at 17:48):
I force-pushed to this branch and Github doesn't update the PR
Eric Wieser (Jun 07 2023 at 17:53):
Last updated: Dec 20 2023 at 11:08 UTC