Re: make world and install-world without docs

[Peter Eisentraut]

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.)