*.old files are now removed by the HTML user manual cleaning script.
Authored by: bugman 2011-01-21
Parent: [r12422]
Child: [r12424]
