commit 7eaed5cd3f5b42b7280897c68ab2e9c0dcd74141
author Davide Pesavento <davidepesa@gmail.com> Wed Jan 09 20:03:43 2019 -0500
committer Davide Pesavento <davidepesa@gmail.com> Wed Jan 09 21:14:02 2019 -0500
tree d435eb04d97d31722f703206f0f3e4d706f3a631
parent 51459409bdc2c70fe7804eb6df7a0917cb0c1259

Update build system and CI scripts

Change-Id: I4894a30d0cfc7af5de1d272edb70ce9cc4b6d372

.jenkins.d/10-build.sh

diff --git a/.jenkins.d/10-build.sh b/.jenkins.d/10-build.sh
index 5a8a7f5..97bc518 100755
--- a/.jenkins.d/10-build.sh
+++ b/.jenkins.d/10-build.sh
@@ -1,10 +1,14 @@
 #!/usr/bin/env bash
 set -e
+
+JDIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
+source "$JDIR"/util.sh
+
 set -x
 
-sudo env "PATH=$PATH" ./waf --color=yes distclean
+sudo_preserve_env PATH -- ./waf --color=yes distclean
 
 ./waf --color=yes configure
 ./waf --color=yes build -j${WAF_JOBS:-1}
 
-sudo env "PATH=$PATH" ./waf --color=yes install
+sudo_preserve_env PATH -- ./waf --color=yes install