Thanks for looking into this. I have made a different but equivalent fix that I will check in as soon as my ISP gets it head out of its rear end.