Re: HTML format documentation

[Richard Stallman]

Whether to use /usr/share/doc instead of /usr/doc is a decision I will
have to think about.  "Standards" written for the GNU system by people
who are not participating in the GNU Project, and who don't even
recognize that the system is GNU, have no authority here.  Please do
not change this now.

However, adding --docdir seems like a natural thing.