Re: Changing the HTML file extension

Vince Vielhaber <vev@michvhf.com> writes:
> [ a long list of places that might have links to documentation pages ]

I think this discussion is largely pointless.  We have already made a
substantial number of changes in the filenames of various doc pages
since 7.0 (for instance, there aren't numbers in most of 'em anymore),
and I didn't hear anyone objecting.  Asking that bookmarks not break is
a little late at this point.

I'm for changing to .html, FWIW.

            regards, tom lane