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: May 02 2025 at 03:31 UTC