diff options
| author | Oliver Smith <osmith@sysmocom.de> | 2021-01-13 13:10:55 +0100 |
|---|---|---|
| committer | Oliver Smith <osmith@sysmocom.de> | 2021-01-13 13:10:55 +0100 |
| commit | 4642ab68278aa2be16c660fc947f36635c46ae2d (patch) | |
| tree | 9cefd0466978f4508a66a5a67c99f683af6a6dd5 | |
| parent | 02830f3bd247ccfe0421782d957d08ebc235f1c6 (diff) | |
contrib/jenkins: don't build osmo-gsm-manuals
Related: OS#4912
Change-Id: If8f88bde0614547bb5c4f4f6e97fc20fcecd8a2c
# ---
| -rwxr-xr-x | contrib/jenkins.sh | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh index 07a02c1a..fafbdfba 100755 --- a/contrib/jenkins.sh +++ b/contrib/jenkins.sh @@ -52,7 +52,6 @@ done # Build and publish manuals if [ "$WITH_MANUALS" = "1" ]; then - osmo-build-dep.sh osmo-gsm-manuals make -C "$base/doc/manuals" make -C "$base/doc/manuals" check |