aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.menhir
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2020-02-05 18:36:08 +0100
committerGitHub <noreply@github.com>2020-02-05 18:36:08 +0100
commit6950ac8fb096768cb3811ae7f89d0db080bf965a (patch)
tree9070ec9c2d6bf1277de5df13366b538f7c381e80 /Makefile.menhir
parentb0fdbb0e88d6decd068709ea673dbe51fd6727b0 (diff)
downloadcompcert-kvx-6950ac8fb096768cb3811ae7f89d0db080bf965a.tar.gz
compcert-kvx-6950ac8fb096768cb3811ae7f89d0db080bf965a.zip
Revised menhirLib autoconfiguration (#331)
Since Menhir version 20200123, we need to link with menhirLib.cmxa instead of menhirLib.cmx. This commit chooses automatically the file to link with: menhirLib.cmxa if it exists in the menhirLib installation directory, menhirLib.cmx otherwise. To reliably find the installation directory, configure was changed to record the menhirLib directory in Makefile.config, variable MENHIR_DIR, instead of a pre-cooked command-line option MENHIR_INCLUDES. Makefile.extr was adapted accordingly. Fixes: #329 Closes: #330
Diffstat (limited to 'Makefile.menhir')
-rw-r--r--Makefile.menhir6
1 files changed, 5 insertions, 1 deletions
diff --git a/Makefile.menhir b/Makefile.menhir
index 98bfc750..7909b2f6 100644
--- a/Makefile.menhir
+++ b/Makefile.menhir
@@ -41,7 +41,11 @@ MENHIR_FLAGS = -v --no-stdlib -la 1
# Using Menhir in --table mode requires MenhirLib.
ifeq ($(MENHIR_TABLE),true)
- MENHIR_LIBS = menhirLib.cmx
+ ifeq ($(wildcard $(MENHIR_DIR)/menhirLib.cmxa),)
+ MENHIR_LIBS = menhirLib.cmx
+ else
+ MENHIR_LIBS = menhirLib.cmxa
+ endif
else
MENHIR_LIBS =
endif