Stream: Coq devs & plugin devs

Topic: coqbot message


view this post on Zulip Matthieu Sozeau (Apr 16 2024 at 22:04):

On this PR I get a curious message I don’t understand: https://github.com/coq/coq/pull/18903 coqbot replies Got more than one checkSuite. When I try to launch a bench

view this post on Zulip Gaëtan Gilbert (Apr 16 2024 at 22:09):

the check in the bot looks like if pipeline_count <> 1 then error "more than 1 checksuite"
the pipeline isn't starting for some reason so pipeline_count is 0
if there is a merge conflict then that's why
if not then IDK, you can try @coqbot run light ci (or full if you want)

view this post on Zulip Théo Zimmermann (Apr 24 2024 at 12:24):

We could refine the message in case there is no check suite.

view this post on Zulip Gaëtan Gilbert (Apr 24 2024 at 12:28):

https://github.com/coq/bot/pull/302


Last updated: Oct 13 2024 at 01:02 UTC