coq / bot

A (Coq Development Team) bot written in OCaml
MIT License
23 stars 14 forks source link

Minimizer gets confused when there are multiple pipelines for the base commit #267

Open SkySkimmer opened 1 year ago

SkySkimmer commented 1 year ago

eg https://github.com/coq/coq/pull/17243#issuecomment-1424342254 it sees https://gitlab.com/coq/coq/-/pipelines/762836836 ("Bot merge 542d3718 and e9c7feda" from the backport testing PR) and https://gitlab.com/coq/coq/-/pipelines/763974119/ (from the actual push to v8.17)

Zimmi48 commented 1 year ago

We could solve this issue by arbitrarily using the first pipeline. Even better, we could check each pipeline to find one that contains all the information we need (e.g., if there was a light pipeline and a full pipeline, or if one of them was cancelled, etc.).