The HTML user manual cleaning script now removes all *.css files.
Authored by: bugman 2011-01-22
Parent: [r12425]
Child: [r12427]
