Jason Gross (May 12 2021 at 12:06): 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.
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: May 28 2023 at 13:30 UTC