jenkins: fix publish

the script argument was not saved in the publish variable used later
to decide if publishing/uploading is needed.

Change-Id: Ic768a8e96e5e4d72acf3979da1412d683f79ec55

contrib/jenkins.sh

@@ -9,6 +9,7 @@ fi
 
 set -e
 
+publish="$1"
 base="$PWD"
 deps="$base/deps"
 inst="$deps/install"