tree ae7a7caeb88edddc7e62cc4ae19f1872cd2e3856
parent 82c1d1eb20f71f2e52de877cd634c126fd0bb991
author Oliver Smith <osmith@sysmocom.de> 1543497629 +0100
committer Oliver Smith <osmith@sysmocom.de> 1544011773 +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: I24179b21ce4ff182649243e286c87c824b889454