From 0674a3535c8861ab608ad0bc57506b83cda8a158 Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Thu, 24 Oct 2019 06:46:43 +0200
Subject: configure: fails if 'make' failed.

---
 configure | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'configure')

diff --git a/configure b/configure
index c6e64b88e..65b010b49 100755
--- a/configure
+++ b/configure
@@ -360,7 +360,10 @@ if ! sh ./config.status; then
 fi
 
 # Create dirs
-$MAKE create-dirs
+if ! $MAKE create-dirs; then
+    echo "$progname: cannot execute $MAKE create-dirs"
+    exit 1
+fi
 
 # Generate ortho_code-x86-flags
 if test $backend = mcode; then
-- 
cgit v1.2.3