contrib/jenkins.sh: ugly work-around for PATH problems

For details see https://osmocom.org/issues/4911

Related: OS#4911
Change-Id: I04e9c29813f6695d0d53f7cdede34f83d24ea3fd
diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh
index 1a0750f..b788540 100755
--- a/contrib/jenkins.sh
+++ b/contrib/jenkins.sh
@@ -5,6 +5,15 @@
 # * WITH_MANUALS: build manual PDFs if set to "1"
 # * PUBLISH: upload manuals after building if set to "1" (ignored without WITH_MANUALS = "1")
 
+# ugly, ugly hack to work around the fact that we cannot _extend_ the path when executing
+# a docker container.  We can either override it (and loose our /opt/... toolchain paths)
+# or we can not specify the /build_bin whcih means the osmo-build-dep.sh is not found
+# See https://osmocom.org/issues/4911
+if [ -d /build_bin ]; then
+	PATH=$PATH:/build_bin
+	export PATH
+fi
+
 if ! [ -x "$(command -v osmo-build-dep.sh)" ]; then
 	echo "Error: We need to have scripts/osmo-deps.sh from http://git.osmocom.org/osmo-ci/ in PATH !"
 	exit 2