Peter Eisentraut <peter.eisentr...@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
