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.

Reply via email to