diff options
author | Oliver Smith <osmith@sysmocom.de> | 2021-01-13 13:16:48 +0100 |
---|---|---|
committer | Oliver Smith <osmith@sysmocom.de> | 2021-01-13 13:16:48 +0100 |
commit | e8edd1fcaec8e159b2c68bf1452616fe9e7c144b (patch) | |
tree | f379812eac8de2d10d0873de41e9798830db945a | |
parent | 7e27deb8cb8ab829d39740225a13fe32a29c7612 (diff) |
contrib/jenkins: don't build osmo-gsm-manuals
Related: OS#4912
Change-Id: Ibacb11da37acfd324cee37068099627136717781
-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 7b751ad..3cf12c6 100755 --- a/contrib/jenkins.sh +++ b/contrib/jenkins.sh @@ -89,7 +89,6 @@ CONFIG="--enable-sanitize --enable-werror --with-uhd --with-usrp1 --with-lms --w # Additional configure options and depends if [ "$WITH_MANUALS" = "1" ]; then - osmo-build-dep.sh osmo-gsm-manuals CONFIG="$CONFIG --enable-manuals" fi |