Stream: coqbot devs & users

Topic: ci secretly finished

view this post on Zulip Gaëtan Gilbert (May 12 2022 at 15:19):

CI on https://github.com/coq/coq/pull/15274 is done but still marked as running

view this post on Zulip Théo Zimmermann (May 12 2022 at 15:44):

Likely an issue with a webhook delivery. Unfortunately, it's impossible to get webhook data from GitLab more than about 24 hours in the past. So it's going to be hard to investigate. But maybe we should have a mechanism actively checking whether a long-running pipeline is actually finished.

view this post on Zulip Ali Caglayan (Jun 06 2022 at 17:36):

coqbot doesn't run unless triggered right?

view this post on Zulip Ali Caglayan (Jun 06 2022 at 17:36):

Maybe it would be good to do a manual trigger for checks twice a day

view this post on Zulip Théo Zimmermann (Jun 06 2022 at 18:14):

Indeed, something similar to what is already done for stale issues.

Last updated: Apr 19 2024 at 04:02 UTC