Hey, one think I'd really like to see is the ability to close PRs on github and/or add labels to PRs. I just noticed, that I revisited the same PR for the third time, because I could not close it.
Maybe gitbox could help there? Greetings Matthias Am Samstag, den 14.10.2017, 14:46 +0200 schrieb Matthias Bläsing: > 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.wielen > > [email protected]> wrote: > > > > > https://issues.apache.org/jira/browse/INFRA-15271 > > > > > > On Fri, Oct 13, 2017 at 1:11 PM, Geertjan Wielenga <geertjan.wiel > > > [email protected]> 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
