Theia build failed after merging plugin metrics

[original thread by Anatoliy Bazko]

Hmh…shouldn’t I get a mail if I merge a PR that breaks the build?

I think so - I have had such emails from Travis in the past. It could be that the author is the one to receive the mail, not the person who merged?

Thank you for taking care about it!

@abazko :slight_smile: