diff options
| author | Oliver Smith <osmith@sysmocom.de> | 2018-11-28 11:33:39 +0100 |
|---|---|---|
| committer | Oliver Smith <osmith@sysmocom.de> | 2018-12-05 13:09:11 +0100 |
| commit | ab9a259cd2e5f0d188ebfecdb2a271e8c0dba94b (patch) | |
| tree | 7a099b40ffa35b31d69bda1ca7d0521cb7be0990 /include | |
| parent | b871da977bf329be115dd8a3e4096beb4148219d (diff) | |
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: Ief6ce94013612a968183e82abef421f116ed37c3
Diffstat (limited to 'include')
0 files changed, 0 insertions, 0 deletions