Disable real builds on jenkins/simgrid-qualif, hoping to avoid conflicts when both...

diff --git a/tools/jenkins/build.sh b/tools/jenkins/build.sh
index 9c8fc76..a9d9d64 100755 (executable)
--- a/tools/jenkins/build.sh
+++ b/tools/jenkins/build.sh
@@ -2,6 +2,13 @@
 
 # This script is used by various build projects on Jenkins
 
+case "$JENKINS_HOME" in
+*-qualif)
+  echo "Build skipped on $JENKINS_HOME."
+  exit 0
+  ;;
+esac
+
 # See https://ci.inria.fr/simgrid/job/SimGrid/configure
 # See https://ci.inria.fr/simgrid/job/Simgrid-Windows/configure