Re: Changing the HTML file extension

Agreed.   *.htm is an old DOS-ism.

> 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/
>
>


--
  Bruce Momjian                        |  http://candle.pha.pa.us
  pgman@candle.pha.pa.us               |  (610) 853-3000
  +  If your life is a hard drive,     |  830 Blythe Avenue
  +  Christ can be your backup.        |  Drexel Hill, Pennsylvania 19026