Well we could remove all push rights to master repos and let the ci bot do the merge.<div><br></div><div>Then it's as prevented as gerrit. </div><div><br></div><div>I believe that's what openshift does. But they have actual integration tests too :)</div><div><br></div><div>But yes gerrit has nicer flow overall. <span></span></div><div><br></div><div>/max <br><br>On Wednesday, 22 June 2016, Mickael Istria <<a href="mailto:mistria@redhat.com">mistria@redhat.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
<div>On 06/22/2016 05:20 PM, Jean-Francois
Maury wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">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 ?<br>
</div>
</blockquote>
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.<br>
Once again, Gerrit does it better :P<br>
<div>-- <br>
Mickael Istria<br>
Eclipse developer at <a href="http://www.jboss.org/tools" target="_blank">JBoss,
by Red Hat</a><br>
<a href="http://mickaelistria.wordpress.com" target="_blank">My blog</a> - <a href="http://twitter.com/mickaelistria" target="_blank">My Tweets</a></div>
</div>
</blockquote></div><br><br>-- <br><div dir="ltr"><div>/max<br></div><a href="https://about.me/maxandersen" target="_blank">https://about.me/maxandersen</a><br></div><br>