Fix: tools: Set a title for HTML output.
Don't just use the command line, which is less helpful for HTML.