Commit e12a471f6af23257f4c406feb8745eb12915fa7d

Werner Lemberg 2006-05-12T14:20:43

* src/tools/docmaker/tohtml.py (html_header_1): Use `utf-8' charset. Convert some files to UTF-8.