Hi Thomas,
I think the root cause in this case was that the PR had sat a couple of years un-merged, and so had become stale. Ci had passed at the time and there were no merge conflicts, so it looked good to merge. In such a case, I think we should re-trigger CI, which
I think would have caught the issue (I think CI tests the PR merged on top of latest master but I am not sure if it would redo the merge upon being re-triggered. So maybe the PR would need to be uplifted first?)
Regards,
Marc
From: theia-dev <theia-dev-bounces@xxxxxxxxxxx> on behalf of Thomas Mäder <t.s.maeder@xxxxxxxxx>
Sent: Thursday, March 16, 2023 10:09 AM
To: theia-dev@xxxxxxxxxxx <theia-dev@xxxxxxxxxxx>
Subject: [theia-dev] Master breakage
Hi folks,
we recently merged https://github.com/eclipse-theia/theia/pull/10338,
which seems to have broken master. Mistakes happen, but I'm wondering if we can improve our process? Did the linter check fail and we merged anyway, or is there some technical improvement we can make?
I'd also would encourage anyone who is involved in a "master is broken"-situation to write a quick mail to this very list to alert the community. It keeps everyone with failing PR's from having to investigate
what's wrong themselves.
thanks,
/Thomas
|