Yeah, I agree, it may be easier to review for some reviewers because they don’t need to to spend time looking up the rules. But given that it has been merged (i.e., review has been done), I don’t think it’s worth spending a PR on this. Feel free to open a PR if you disagree.
(Sorry, I hadn’t seen your comment earlier. I was spending some time testing this locally before pushing the merge. Your comment arrived after I had created the merge commit locally, but I believe before I pushed it. Then I didn’t check github again before pushing the merge.)