From 69de1fb05c13c742a5ec369ed074841654b74856 Mon Sep 17 00:00:00 2001
From: Tomas Oberhuber <tomas.oberhuber@fjfi.cvut.cz>
Date: Wed, 20 Nov 2019 17:00:20 +0100
Subject: [PATCH] Scipts install and build end with error code when build
 fails.

---
 build   |  4 +++-
 install | 10 ++++++++--
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/build b/build
index 914c65b197..68966f0f42 100755
--- a/build
+++ b/build
@@ -202,7 +202,9 @@ if [[ "$make" != "make" ]] && [[ "$VERBOSE" ]]; then
    VERBOSE="-v"
 fi
 
-$make ${VERBOSE} $make_target
+if ! $make ${VERBOSE} $make_target; then
+   exit 1
+fi
 
 if [[ ${WITH_DOC} == "yes" ]]; then
    "$ROOT_DIR/Documentation/build" --prefix="$PREFIX"
diff --git a/install b/install
index fe138dfaa0..9b66bfbeec 100755
--- a/install
+++ b/install
@@ -35,7 +35,10 @@ if [[ ${BUILD_DEBUG} == "yes" ]]; then
       mkdir Debug
    fi
    pushd Debug
-   ../build --root-dir=.. --build=Debug --install=yes ${OPTIONS}
+   if ! ../build --root-dir=.. --build=Debug --install=yes ${OPTIONS}; then
+      echo "Debug build failed."
+      exit 1
+   fi
    popd
 fi
 
@@ -44,7 +47,10 @@ if [[ ${BUILD_RELEASE} == "yes" ]]; then
       mkdir Release
    fi
    pushd Release
-   ../build --root-dir=.. --build=Release --install=yes ${OPTIONS};
+   if ! ../build --root-dir=.. --build=Release --install=yes ${OPTIONS}; then
+      echo "Release build failed."
+      exit 1
+   fi
    popd
 fi
 
-- 
GitLab