Here is an updated version of the patch. It has your fix suggestion and it also adds the proper character set header to the HTML file. It assumes that HTML output is always UTF-8.
Here is an updated version of the patch. It has your fix suggestion and it also adds the proper character set header to the HTML file. It assumes that HTML output is always UTF-8.