Re: make world and install-world without docs

Peter Eisentraut <peter.eisentraut@enterprisedb.com> writes:
> On 31.05.21 16:16, Andrew Dunstan wrote:
>> make SKIPDOCS=1 world
>> make SKIPDOCS=1 install-world

> Maybe this should be configure option?  That's generally where you set 
> what you want to build or not build.  (That might also make the 
> buildfarm integration easier, since there are already facilities to 
> specify and report configure options.)

Hmm, I think I prefer Andrew's way.  The fact that I don't want
to build the docs right now doesn't mean I won't want to do so
later --- in fact, that sequence is pretty exactly what I do
whenever I'm working on a patch.  It'd be annoying to have
to re-configure to make that work.

            regards, tom lane