JasonGross
commented
2 years ago Criterion for outdated:
- Any "Minimization is available" should hide all previous "minimization is available" on the same PR
- Any "I'm starting minimization" should hide all previous "minimization is available"
- Any "I have minimization results for ci-XXX" should hide all previous results for ci-XXX, and all previous "I'm starting minimization" if there are already results for all projects other than ci-XXX mentioned in that comment that occur between the "starting" comment and the present time (or perhaps track relatedness by upcoming uids of runs)
Take https://github.com/coq/coq/pull/15220 , I got spammed a lot. In order to make the thread "readable" I did manually mark all old coqbot messages as outdated. IMO the bot could do that automatically when posting a new message.