contrib/jenkins.sh: build and publish manuals
commit60e402d13a142e4a9587d1ce284e7c49ba2fe1a7
authorOliver Smith <osmith@sysmocom.de>
Fri, 7 Dec 2018 13:30:26 +0000 (7 14:30 +0100)
committerOliver Smith <osmith@sysmocom.de>
Wed, 12 Dec 2018 13:07:39 +0000 (12 14:07 +0100)
tree426bf36a1c3fa3b022ad4ff45c4078cf76be1206
parent810b696b8d5d0b8a2c8bb0a596d34e43f4de764c
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: I856e4bc71e1b648de5f27d4044aa60bd0b45e0f5
contrib/jenkins.sh