
<html>

  <head>

    <meta content="text/html; charset=utf-8" http-equiv="Content-Type">

  </head>

  <body text="#000000" bgcolor="#FFFFFF">

    <div class="moz-cite-prefix">On 06/22/2016 05:20 PM, Jean-Francois

      Maury wrote:<br>

    </div>

    <blockquote

cite="mid:CAG6Rg+nBpo89bF27hT43AXgn2R_MYkpm93YubibsnkRX56b4hg@mail.gmail.com"

      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 class="moz-signature">-- <br>

      Mickael Istria<br>

      Eclipse developer at <a href="http://www.jboss.org/tools">JBoss,

        by Red Hat</a><br>

      <a href="http://mickaelistria.wordpress.com">My blog</a> - <a

        href="http://twitter.com/mickaelistria">My Tweets</a></div>

  </body>

</html>