[theia-dev] Master breakage

[Thomas Mäder <t.s.maeder@xxxxxxxxx>]

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