Oliver Smith 60e402d13a 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		2018-12-12 14:07:39 +01:00
..
jenkins.sh	contrib/jenkins.sh: build and publish manuals	2018-12-12 14:07:39 +01:00