From 78accc9375a70d5a37f9b43843d8ac1e973f0968 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 11 Jan 2023 09:12:27 +0100
Subject: [PATCH] [install] allows to use FRAMAC_INSTALLDIR when PREFIX is
 undefined

---
 share/Makefile.common | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/share/Makefile.common b/share/Makefile.common
index 8754621da7b..9df6e730ee1 100644
--- a/share/Makefile.common
+++ b/share/Makefile.common
@@ -54,12 +54,16 @@ PLATFORM:=$(shell uname -s)
 #############
 
 ifndef PREFIX
+ifdef FRAMAC_INSTALLDIR
+PREFIX=$(FRAMAC_INSTALLDIR)
+else
 ifdef OPAM_SWITCH_PREFIX
 PREFIX=$(OPAM_SWITCH_PREFIX)
 else
 PREFIX=/usr/local
 endif
 endif
+endif
 
 #############
 # Verbosing #
-- 
GitLab