Yeah, merged, thanks!

In future: If you have a trivial PR there's no need to open a separate issue. We're not paid by the issue number and it really doesn't add much.

If you expect discussion of the kind of solution (so not slightly adjusting the check but doing an entirely different thing to solve the problem), then sure, open an issue. But this is fairly black and white so one thing open suffices.