AFAIK, there is no easy way on GitHub to automatically prevent a commit from being merged via GitHub UI. So at the moment, taking build results into account is the duty of the individual who wants to merge the patch.Will it be part of our merge workflow ie merging the PR won't be allowed if the status is not green or has it to be manually by the merger ?