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(at)gmx(dot)net http://yi.org/peter-e/
>
>

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