commit 6a81b77260df05b43b28f572b0b52d35842f6305
author Davide Pesavento <davide.pesavento@lip6.fr> Sun Aug 20 18:43:46 2017 -0400
committer Davide Pesavento <davide.pesavento@lip6.fr> Sat Aug 26 17:06:00 2017 -0400
tree 37f71d53687b241ebcae0fa135b44dec421f758e
parent c0c6bcf7e29cf477659cbc31c67082e054f42742

ci: preserve PATH when running waf under sudo

Change-Id: I85bdc5b69de2c2c7b8c0dc5a7aa2927b495e2168
Refs: #4186

.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}
 }