[jenkins] Workaround for Windows

diff --git a/buildtools/jenkins/build.sh b/buildtools/jenkins/build.sh
index 1d1618b..f79bd10 100755 (executable)
--- a/buildtools/jenkins/build.sh
+++ b/buildtools/jenkins/build.sh
@@ -9,6 +9,25 @@ done
 echo "Build mode was $build_mode" >&1
 
 build_mode="$1"
+case "$build_mode" in
+  "Debug")
+  ;;
+
+  "ModelChecker")
+  ;;
+
+  "DynamicAnalysis")
+  ;;
+
+  *)
+    if "$(uname -o)" = "Msys"; then
+      echo "On Windows, jenkins is not willing to expand variables for some reason" >&2
+      echo "Force use Debug mode" >&2
+    else
+      die 1 "Unknown build_mode $build_mode"
+    fi
+  ;;
+esac
 echo "Build mode $build_mode on $(uname -np)" >&2
 
 if test "$(uname -o)" = "Msys"; then
@@ -48,21 +67,6 @@ fi
 mkdir $WORKSPACE/build
 cd $WORKSPACE/build
 
-case "$build_mode" in
-  "Debug")
-  ;;
-
-  "ModelChecker")
-  ;;
-
-  "DynamicAnalysis")
-  ;;
-
-  *)
-  die 1 "Unknown build_mode $build_mode"
-  ;;
-esac
-
 cmake -G"$GENERATOR" -Denable_documentation=OFF $WORKSPACE
 make dist -j$NUMBER_OF_PROCESSORS
 tar xzf `cat VERSION`.tar.gz