From cd4eb15c40cdcac3d3269ed4f64eb870ec370823 Mon Sep 17 00:00:00 2001
From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Mon, 27 Jul 2015 16:42:34 +0200
Subject: [PATCH] [jenkins] Check build mode before making the archive

---
 buildtools/jenkins/build.sh | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/buildtools/jenkins/build.sh b/buildtools/jenkins/build.sh
index 125d3ca109..3af2e9499b 100755
--- a/buildtools/jenkins/build.sh
+++ b/buildtools/jenkins/build.sh
@@ -47,11 +47,6 @@ fi
 mkdir $WORKSPACE/build
 cd $WORKSPACE/build
 
-cmake -G"$GENERATOR" -Denable_documentation=OFF $WORKSPACE
-make dist -j$NUMBER_OF_PROCESSORS
-tar xzf `cat VERSION`.tar.gz
-cd `cat VERSION`
-
 case "$build_mode" in
   "Debug")
   ;;
@@ -67,6 +62,11 @@ case "$build_mode" in
   ;;
 esac
 
+cmake -G"$GENERATOR" -Denable_documentation=OFF $WORKSPACE
+make dist -j$NUMBER_OF_PROCESSORS
+tar xzf `cat VERSION`.tar.gz
+cd `cat VERSION`
+
 cmake -G"$GENERATOR"\
   -Denable_debug=ON -Denable_documentation=OFF -Denable_coverage=OFF \
   -Denable_model-checking=$(onoff test "$build_mode" = "ModelChecker") \
-- 
2.20.1