You can also push up the commits to a separate branch, which closes the PR, then delete that branch (note you have to eventually push a real commit on top so there will be a short delay until someone commits to git in a non-delete fashion).
John On Mon, Oct 24, 2016 at 4:25 PM Clebert Suconic <clebert.suco...@gmail.com> wrote: > On Mon, Oct 24, 2016 at 10:39 AM, Christopher Shannon > <christopher.l.shan...@gmail.com> wrote: > > I don't really like the idea of empty commits laying around. It would be > > nice if infra could give us permission somehow to actually close these > > commits on github. > > +1 > > although I can see why Infra is doing that. > > there's a fork update through the apache bot (the github fork is in > sync with the apache git), and if someone pushes the "merge" button on > github by accident, a lot of stuff would probably be broken? > > There's no way (afaik) to only permit closing a PR. You would get all > or nothing. > > > But if we could have at least one person on our group with that power. > (Bruce maybe?) we would speed up the process IMO. >
