Although it is a lot of work to go through all the PRs one way is to ask the submitter to close the PR. If not done after say a week, simply close it. Not sure if this can be done without this #magic at github ... On Mar 24, 2015 1:14 AM, "Paul Davis" <[email protected]> wrote:
> Hi all, > > I've been going through trying to review open PRs today (long overdue, I > know) and I've noticed that there seem to be a lot of "open" PRs that have > actually been merged. Did we ever find a way to be able to close PRs > wihtout having to add a commit with the "Fixes #whatever" magic? > > Paul >
