diff --git a/contrib/jenkins.sh b/contrib/jenkins.sh
index bf755b6e..5ce59931 100755
--- a/contrib/jenkins.sh
+++ b/contrib/jenkins.sh
@@ -9,6 +9,7 @@ fi
 
 set -e
 
+publish="$1"
 base="$PWD"
 deps="$base/deps"
 inst="$deps/install"