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
