diff --git a/share/Makefile.common b/share/Makefile.common index 8754621da7b77f997fcd326615908992472087f9..9df6e730ee14759532d4f61f964b483d9e5ac258 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 #