Stream: coqbot devs & users

Topic: pipeline skipped?


view this post on Zulip Gaëtan Gilbert (Jul 01 2020 at 09:42):

For some reason no gitlab pipe was run for https://github.com/coq/coq/pull/12615 (azure did run so the checks show green).
What is going on?

view this post on Zulip Théo Zimmermann (Jul 01 2020 at 17:23):

Thanks for reporting! It looks like since I merged coq/bot#60, some webhook deliveries occasionally time out. I'll investigate more but in the meantime, I'll deploy an older, virtually functionally equivalent version of the bot.


Last updated: Jan 31 2023 at 10:01 UTC