diff options
| author | Oliver Smith <osmith@sysmocom.de> | 2018-11-29 14:16:27 +0100 |
|---|---|---|
| committer | Oliver Smith <osmith@sysmocom.de> | 2018-12-05 13:16:14 +0100 |
| commit | 33c537e5a756d3390f454968dda5ab14b98e2314 (patch) | |
| tree | ea8a56791747b1a27f13a20ad84501406bdea571 /debian/libgtp3.install | |
| parent | aa69034c00dbbc0c8d1dbfcb5bbadf96d38141a5 (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: I43e3b592c593237eb4df2d70c926c031ddb7b20b
Diffstat (limited to 'debian/libgtp3.install')
0 files changed, 0 insertions, 0 deletions