commit 956ac311b89800e5d20b3b3eee757f2385bad9ea
author Davide Pesavento <davide.pesavento@lip6.fr> Tue Sep 20 19:11:30 2016 +0200
committer Davide Pesavento <davide.pesavento@lip6.fr> Tue Sep 20 19:11:30 2016 +0200
tree f816ecc65a630dbcbd609c60a81aba7dcb6b0c34
parent 525c1071b1ef2d012b832b6b160992f732c5a721

ci: sync jenkins scripts with NFD

Change-Id: I43689bcf51bbe7a1c3118d8b0c226b56077fb4ed

.jenkins.d/util.sh

diff --git a/.jenkins.d/util.sh b/.jenkins.d/util.sh
old mode 100755
new mode 100644
index 81c8931..a89bc27
--- a/.jenkins.d/util.sh
+++ b/.jenkins.d/util.sh
@@ -1,9 +1,18 @@
 has() {
+    local saved_xtrace
+    [[ $- == *x* ]] && saved_xtrace=-x || saved_xtrace=+x
+    set +x
+
     local p=$1
     shift
-    local x
-    for x in "$@"; do
-        [[ "${x}" == "${p}" ]] && return 0
+    local i ret=1
+    for i in "$@"; do
+        if [[ "${i}" == "${p}" ]]; then
+            ret=0
+            break
+        fi
     done
-    return 1
+
+    set ${saved_xtrace}
+    return ${ret}
 }