tree bf411163c4a17e7f6b660df3788f614de9de54e8
parent 117d7a963441c27d98a083c54692c5b8765779d5
author Oliver Smith <osmith@sysmocom.de> 1544191246 +0100
committer Oliver Smith <osmith@sysmocom.de> 1544620135 +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.

Related: OS#3385
Change-Id: I89be11d346d50169282c991235ffc47dacc30b11