make world and install-world without docs

I've been thinking about rationalizing some of the buildfarm code, which
has grown somewhat like Topsy over the years. One useful thing would be
to run all the "make" and "install" pieces together. When the buildfarm
started we didn't have world targets, but they are now almost ancient
history themselves, so it would be nice to leverage them.

However, not all buildfarm animals are set up to build the docs, and not
all owners necessarily want to. Moreover, we have provision for testing
various docs formats (PDF, epub etc). So I'd like to be able to build
and install all the world EXCEPT the docs. Rather than specify yet more
targets in the Makefile, it seemed to me a better way would be to
provide a SKIPDOCS option that could be set on the command line like this:

    make SKIPDOCS=1 world
    make SKIPDOCS=1 install-world

The attached very small patch is intended to provide for that.
Incidentally, this is exactly what the MSVC build system's 'build.bat'
and 'install.bat' do.

I should add that quite apart from the buildfarm considerations this is
something I've long wanted, and I suspect other developers would find it
useful too.

Obviously to be useful to the buildfarm it would need to be backpatched.


cheers


andrew

--
Andrew Dunstan
EDB: https://www.enterprisedb.com