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

Peter Eisentraut <peter_e(at)gmx(dot)net> writes:
> 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.

Well, having "make install" behave in a history-dependent fashion is just
as much a hazard for users as it is for developers.

regards, tom lane