Minimizer gets confused when there are multiple pipelines for the base commit
SkySkimmer opened this issue · 1 comments
SkySkimmer commented
eg coq/coq#17243 (comment)
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
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.).