Hash : e12a471f Author : Date : 2006-05-12T14:20:43
* src/tools/docmaker/tohtml.py (html_header_1): Use `utf-8' charset. Convert some files to UTF-8.