From e26ae15e8a8211353e549d60b7fc731ff72d6498 Mon Sep 17 00:00:00 2001
From: Jean-Baptiste Keck <Jean-Baptiste.Keck@imag.fr>
Date: Fri, 6 Oct 2017 11:08:17 +0200
Subject: [PATCH] added makefile check

---
 ci/scripts/build.sh  | 5 ++++-
 ci/scripts/config.sh | 5 +++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/ci/scripts/build.sh b/ci/scripts/build.sh
index 47de28284..687bb282f 100644
--- a/ci/scripts/build.sh
+++ b/ci/scripts/build.sh
@@ -14,7 +14,10 @@ fi
 BUILD_FOLDER="$1"
 mkdir -p $BUILD_FOLDER
 cd $BUILD_FOLDER
-
+if [ ! -f Makefile ]; then
+    echo "The makefile has not been generated."
+    exit 1
+fi
 CC="$2" CXX="$3" FC="$4" make VERBOSE=1 .. 
 
 exit 0
diff --git a/ci/scripts/config.sh b/ci/scripts/config.sh
index 4fbf3b54e..58ffefdaf 100644
--- a/ci/scripts/config.sh
+++ b/ci/scripts/config.sh
@@ -18,4 +18,9 @@ mkdir -p $BUILD_DIR
 cd $BUILD_DIR
 CC="$2" CXX="$3" FC="$4" cmake -DCMAKE_BUILD_TYPE=Release $ROOT_DIR
 
+if [ ! -f Makefile ]; then
+    echo "The makefile has not been generated."
+    exit 1
+fi
+
 exit 0
-- 
GitLab