tree 8a9cba121ca783d046b85eacecadd9a8ae467ce2
parent 61469d1d86b6a347823efecffa037997b1cd08da
author Oliver Smith <osmith@sysmocom.de> 1543499848 +0100
committer Oliver Smith <osmith@sysmocom.de> 1544014046 +0100

contrib/jenkins.sh: build and publish manuals

Add new environment variables WITH_MANUALS and PUBLISH to control if
the manuals should be built and uploaded. Describe all environment vars
on top of the file.

When WITH_MANUALS is set, install osmo-gsm-manuals like any other
dependency and add --enable-manuals to the configure flags (for "make"
and "make distcheck"). Add the bin subdir of the installed files to
PATH, so osmo-gsm-manuals-check-depends can be used by ./configure.

Related: OS#3385
Change-Id: Ia5b112fc1663b78800d3c2c4ff2a0771cf5af11b