From acdf2896767110434ab9535eee0abb06c42b7cd3 Mon Sep 17 00:00:00 2001
From: Martin Quinson <martin.quinson@loria.fr>
Date: Mon, 16 Apr 2018 00:23:11 +0200
Subject: [PATCH] painful typo(s)

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

diff --git a/tools/jenkins/build.sh b/tools/jenkins/build.sh
index 1ce50ae751..7f98d0f7fb 100755
--- a/tools/jenkins/build.sh
+++ b/tools/jenkins/build.sh
@@ -126,9 +126,9 @@ echo "XX Configure and build SimGrid"
 echo "XX   pwd: "$(pwd)
 echo "XX"
 set -x
-if [ "$build_mode" = "ModelChecker" ] ;
+if [ "$build_mode" = "ModelChecker" ] ; then
    INSTALL="-DCMAKE_INSTALL_PREFIX=/builds/mc_simgrid_install"
-elif [ "$build_mode" = "Debug" ] ;
+elif [ "$build_mode" = "Debug" ] ; then
    INSTALL="-DCMAKE_INSTALL_PREFIX=/builds/simgrid_install"
 fi
 cmake -G"$GENERATOR" $INSTALL \
-- 
2.20.1