Gaëtan Gilbert (Jul 01 2020 at 09:42): 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?
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: Sep 15 2024 at 12:01 UTC