Improve accuracy. In the .tex file, note the new "% BUG:" comments: an

extra backslash is getting displayed in the generated HTML.