The HTML files for the user manual now have longer names - this is needed for removing the duplicates.
Authored by: bugman 2012-09-19
Parent: [r17514]
Child: [r17516]
