Since I'm writing a custom stylesheet for the docs anyway, we could change
the extension of the HTML files from .htm to .html. This will probably
break a lot of bookmarks, so I thought I'd ask. OTOH, "deep" bookmarks
into the current docs may become obsolete for a variety of other reasons
anyway.
--
Peter Eisentraut peter_e@gmx.net http://yi.org/peter-e/
