Re: "make install" now tries to build the documentation

On tis, 2009-08-18 at 14:32 -0400, Tom Lane wrote:
> I'm leaning more towards the "make install-docs" solution after further
> thought.  One thing that's always been a bit bogus about make install
> is that it installs the docs only if they're there.  With a separate
> top-level target, it would be reasonable to throw an error if the
> docs aren't there and can't be built.

I don't think we should impose an additional burden on the users because
of some glitches in the workflow of some developers.  There can be
another solution.  We can add an option or a make target or whatever to
refine the behavior in a developer environment.

I'm not exactly sure what the goal is, however.  You built the
documentation at some point.  Then it gets updated when necessary.  You
can delete the documentation by running make -C doc maintainer-clean.
Then it's gone forever and never reappears unless you explicitly build
it again.