From bf906c55393fdc6378cc261c4c2fccf083a75c1d Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 17 Jan 2017 11:22:45 +0100
Subject: [PATCH] Bugfix: create mini-gmp library in distribution

---
 src/plugins/e-acsl/Makefile.in | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 77837f8be73..e040d56b405 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -149,6 +149,7 @@ CPPGMPFLAGS += -Drealloc=__e_acsl_native_realloc
 CPPGMPFLAGS += -Dfree=__e_acsl_native_free
 
 $(EACSL_GMP_LIB): $(EACSL_GMP_DIR)/mini-gmp/mini-gmp.c
+	$(MKDIR) $(EACSL_LIBDIR)
 	echo 'CC          $< '
 	$(CC) $< $(CPPGMPFLAGS) -c -O2 -g3 -o$(EACSL_GMP_MINI)
 	echo 'AR          $@'
-- 
GitLab