From 385adb7672fb42972c8585e7aea13c3c4ec4fcf4 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 12 Jul 2022 16:24:15 +0200
Subject: [PATCH] [configure] use --prefix argument during 'make install'

---
 .gitignore   | 1 +
 Makefile     | 1 +
 configure.ac | 6 ++++--
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/.gitignore b/.gitignore
index 49567453cf9..fcfa3add4da 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,6 +29,7 @@ autom4te.cache
 .log.autoconf
 /.depend
 /config.log
+/config.prefix
 /config.status
 /frama-c*.tar.gz
 /distributed
diff --git a/Makefile b/Makefile
index 4a4fc309266..0e24cbe6416 100644
--- a/Makefile
+++ b/Makefile
@@ -123,6 +123,7 @@ force-reconfigure:
 # INSTALL/UNINSTALL
 ################################
 
+sinclude config.prefix
 FRAMAC_INSTALLDIR?=
 
 INSTALLDIR:=$(FRAMAC_INSTALLDIR)
diff --git a/configure.ac b/configure.ac
index 21b7763b5b5..2484ebf7d2c 100644
--- a/configure.ac
+++ b/configure.ac
@@ -88,8 +88,10 @@ fi
 # Check for invalid command-line options #
 ##########################################
 case $prefix in
-  *\ * ) AC_MSG_ERROR(spaces not allowed in --prefix argument "$prefix");;
-  * ) ;;
+  *\'*|*\"* ) AC_MSG_ERROR(quotes not allowed in --prefix argument: $prefix);;
+  * )
+    echo "FRAMAC_INSTALLDIR?=\"$prefix\"" > config.prefix
+    ;;
 esac
 
 #############################
-- 
GitLab