UTILITIES: Use a separate css for the HTML manuals.