On 06/22/2016 05:20 PM, Jean-Francois Maury wrote:
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 ?
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.
Once again, Gerrit does it better :P
--
Mickael Istria
Eclipse developer at JBoss, by Red Hat <
http://www.jboss.org/tools>
My blog <
http://mickaelistria.wordpress.com> - My Tweets
<
http://twitter.com/mickaelistria>