Re: make world and install-world without docs

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