Hey, Am Freitag, den 13.10.2017, 13:25 +0200 schrieb Geertjan Wielenga: > Or maybe we should vote on this as a community before going ahead > with it? > > Gj > > On Fri, Oct 13, 2017 at 1:23 PM, Geertjan Wielenga > <geertjan.wiele...@googlemail.com> wrote: > > > https://issues.apache.org/jira/browse/INFRA-15271 > > > > On Fri, Oct 13, 2017 at 1:11 PM, Geertjan Wielenga > > <geertjan.wiele...@googlemail.com> wrote: > > > > [Better github integration via gitbox]
I can live with the current situation. I have github as a separate remote and can thus do direct merges from github PRs (they are exposed as branches). On the other hand - especially small changes can be easier integrated with github integration (just one click...). I have no strong opinion either way. Greetings Matthias
