Changing the HTML file extension

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/