diff options
author | Oliver Smith <osmith@sysmocom.de> | 2021-01-13 13:09:09 +0100 |
---|---|---|
committer | Oliver Smith <osmith@sysmocom.de> | 2021-01-13 13:09:09 +0100 |
commit | 73790ba26b2034a01790b5830e423d770caad272 (patch) | |
tree | 40231f5a90999b0a2310099ef1614ccccc8c30a2 /contrib | |
parent | 2cdf1c37a93ec7e8c9de1ae7cf3ce54a0fd30475 (diff) |
contrib/jenkins: don't build osmo-gsm-manuals
Related: OS#4912
Change-Id: Idb3b05412b99484f7f7de91ee96c69bfb4e3d511
Diffstat (limited to 'contrib')
-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 da8703a22..4b9d532c1 100755 --- a/contrib/jenkins.sh +++ b/contrib/jenkins.sh @@ -54,7 +54,6 @@ build_project() { # Build and publish manuals if [ "$WITH_MANUALS" = "1" ]; then # Build all manuals first - osmo-build-dep.sh osmo-gsm-manuals for dir in "$base"/manuals/*/; do make -C "$dir" done |