[jbosstools-dev] CI jobs building PR

[Mickael Istria]

On 06/22/2016 06:44 PM, Max Andersen wrote:
> Well we could remove all push rights to master repos and let the ci 
> bot do the merge.
You mean a CI bot that would merge on developer request? If so I don't 
get how it's better than leaving the developer push directly.
> Then it's as prevented as gerrit.
Usually, Gerrit UI simply hides the "Submit" button on a contribution if 
it doesn't conform to project requirements (fast-forward, Verified+1, 
Code-Review+2, no -1). AFAIK, there is no way to add such logic on 
GitHub UI and the Merge button is always there, even when no-one likes it.

Note that usually with Gerrit, it's still possible for committers to 
push directly to master.
But indeed, some projects do lock master and only allow submission via 
Gerrit UI. Would GitHub allow that? Would it be good to use it given the 
limitation explained above (no way to control the availability of the 
merge operation in UI) ?

-- 
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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.jboss.org/pipermail/jbosstools-dev/attachments/20160622/cb634e18/attachment.html