tree f1fdc8b82fc1a69041492f36ceb6067f5e850488
parent bc9bead62afb31844e80d5a8813abcd9ad82a6f7
author Oliver Smith <osmith@sysmocom.de> 1543413445 +0100
committer Oliver Smith <osmith@sysmocom.de> 1544011687 +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: Ia1a6ab64c7912f30a693ca4f5f474f22d72b8873