Stream: Coq devs & plugin devs

Topic: coqbot CI minimize


view this post on Zulip Jason Gross (May 12 2021 at 12:06):

I've deployed an updated version of coqbot that will inform PR authors when autominimization is available and will respond to @coqbot CI minimize (capitalization of CI does not matter) to run minimization.

view this post on Zulip Jason Gross (May 17 2021 at 00:31):

Temporarily disabled, because I'm not sure how to retrieve relevant PR info from non-PR-review comments. I'll re-enable it once @Théo Zimmermann or someone else lets me know what I should be doing at https://github.com/Zimmi48/bot/blob/faddaa3ea924e3e44ab575e8de0b261ae3970ce9/src/actions.ml#L1208-L1229


Last updated: Oct 21 2021 at 21:03 UTC