Re: [jbosstools-dev] CI jobs building PR
Well we could remove all push rights to master repos and let the ci bot do
the merge.
Then it's as prevented as gerrit.
I believe that's what openshift does. But they have actual integration
tests too :)
But yes gerrit has nicer flow overall.
/max
On Wednesday, 22 June 2016, Mickael Istria <mistria(a)redhat.com> wrote:
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>
--
/max
https://about.me/maxandersen
Attachments:
- attachment.html (text/html — 1.7 KB)