Coverage tool: output HTML files use default encoding instead of UTF-8 or the source encoding

[rliesenfeld]

For an UTF-8 encoded ".java" file containing non-ASCII characters, the generated ".html" file does not get encoded as UTF-8; same happens with index.html.

Either convert whatever the input encoding is to UTF-8, or keep the input encoding in the output file. UTF-8 is the only viable option for index.html, though.