is the 5 intentional?
seems a cat-on-keyboard issue
Fat fingers symptom? ;-)
It sure seems unrelated to the other changes in that commit... I'm tempted to just fix it (since I have commit rights there, I think) but it seems only fair to leave it for @alexmiller’s amusement 🙂
fixed, surely an errant typo :)