I leave a comment. If there's no response, I edit the question to remove the answer and make it a community wiki answer.

I understood this to be standard practice. Since you can fix it yourself, there's no need to bother mods unless there's some other issue.