[JestUM]

Was unable to merge PRs.

Earlier, I also got GitHub PR comment emails about 6 hours late.

Whatever it is, it’s been happening for more than 6 hours.

[toastal]

Could you apply the patch from the URL? Pull requests aren't really needed.