Peter Eisentraut <peter_e@gmx.net> writes:
> On tor, 2010-03-04 at 17:53 +0000, Lou Picciano wrote:
>> ./configure --no-docs or ./configure --with-htmldocs-only
> But that would be a negative regression for end users, who we want to
> have the docs available by default, so they can read them.
"End users" in that sense would almost certainly be working from a
distribution tarball, if not a prepackaged distro. I don't think
this discussion is about them; it's about what is most convenient
for developers. As a developer, I don't find the current arrangement
convenient in the least.
What I'd be for is breaking the docs out as a separate top-level target,
ie "make docs", "make install-docs". I don't much care for Lou's
suggestion of tying it to a configure option because that imposes the
significant additional cost of re-configuring when I change my mind.
I do need to be *able* to build the docs, I just don't want it happening
by surprise.
regards, tom lane