From b7b801bffd5c0ac9dc22c6688c489d6c1e18ad0a Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Date: Tue, 11 Jul 2023 18:26:47 +0200
Subject: [PATCH] Disable real builds on jenkins/simgrid-qualif, hoping to
 avoid conflicts when both simgrid and simgrid-qualif are online.

---
 tools/jenkins/build.sh | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/tools/jenkins/build.sh b/tools/jenkins/build.sh
index 9c8fc76470..a9d9d64f6b 100755
--- 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
 
-- 
2.20.1