@kugel- what I don't like with the `@close` method is that it marks the PR as closes rather than merged. IIUC, what using GitHub's buttons, it does work though, so I imagine it might be possible somehow to do that manually too -- but I might be dreaming.