yet another attempt at testing the tuto on jenkins

[simgrid.git] / tools / jenkins / build.sh

diff --git a/tools/jenkins/build.sh b/tools/jenkins/build.sh
index bf88895..0873ca6 100755 (executable)
--- a/tools/jenkins/build.sh
+++ b/tools/jenkins/build.sh
@@ -126,6 +126,7 @@ echo "XX Configure and build SimGrid"
 echo "XX   pwd: "$(pwd)
 echo "XX"
 set -x
 echo "XX   pwd: "$(pwd)
 echo "XX"
 set -x

+export SIMGRID_INSTALL_PATH=/builds/simgrid_install

 cmake -G"$GENERATOR"\
   -DCMAKE_INSTALL_PREFIX=/builds/simgrid_install \
   -Denable_debug=ON -Denable_documentation=OFF -Denable_coverage=OFF \
 cmake -G"$GENERATOR"\
   -DCMAKE_INSTALL_PREFIX=/builds/simgrid_install \
   -Denable_debug=ON -Denable_documentation=OFF -Denable_coverage=OFF \