<snip> > The pedant in me wants to push commit ...
Greetings all, I don't think this is worth the trouble or commit clutter. We've done enough mass commits to last a decade, and should keep them to a minimum and for important things. If someone wants to use &integer; or <type>integer</type>, <type>void</type> or <void/>, or whatever, then let them? Regards, Philip