Re: HTML format documentation

[Richard Stallman]

    I'm OK with having as many --foodir as people might want (and
    actually, I'd like to suggest that we recommend

            ./configure prefix=/usr

This is inconsistent with the normal command line option syntax.
We should stay with -- for consistency.