It was a transient thing. There's a script that we are using to automatically fetch diffs from a PR and apply the diff against the git repo. Patrick changed the way it works last week, and a regression there was PRs are no longer closed automatically.
I believe he has fixed it. Patrick will also write an email about the details of that script soon. On Mon, Feb 3, 2014 at 11:24 AM, Henry Saputra <[email protected]>wrote: > Seems like some merged PRs by Reynold and Patrick did not close the PR > automatically anymore? > > - Henry >
