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