Well we could remove all push rights to master repos and let the ci bot do the merge.<div><br></div><div>Then it&#39;s as prevented as gerrit. </div><div><br></div><div>I believe that&#39;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 &lt;<a href="mailto:mistria@redhat.com">mistria@redhat.com</a>&gt; 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&#39;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>