From 37e7861c4d232d96209defaf8ac2dbfb4d11f242 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?K=C3=A9vin=20Redon?= Date: Tue, 7 Aug 2018 11:22:24 +0200 Subject: [PATCH] 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 | 1 + 1 file changed, 1 insertion(+) 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"