aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.menhir
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-27 09:45:33 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-27 09:45:33 +0100
commitff7aa1352d4171724963bb834e09a6abdf0e630e (patch)
treebe3b7cf8e8d4ceaba6decc2795e03bb5b03160a5 /Makefile.menhir
parentdb1be72f045a377b99788f160362036e4c3e9271 (diff)
downloadcompcert-kvx-ff7aa1352d4171724963bb834e09a6abdf0e630e.tar.gz
compcert-kvx-ff7aa1352d4171724963bb834e09a6abdf0e630e.zip
Allow the MENHIR_INCLUDE path to be set by environment.
Bug 17481
Diffstat (limited to 'Makefile.menhir')
-rw-r--r--Makefile.menhir7
1 files changed, 3 insertions, 4 deletions
diff --git a/Makefile.menhir b/Makefile.menhir
index 74bd14e2..e845352d 100644
--- a/Makefile.menhir
+++ b/Makefile.menhir
@@ -14,7 +14,7 @@
# Executable.
-MENHIR = menhir
+MENHIR = menhir
# This flag can be set to true or false. It controls whether we use
# Menhir's table back-end or code back-end. The table back-end is a
@@ -28,7 +28,7 @@ MENHIR_TABLE = true
ifeq ($(MENHIR_TABLE),true)
MENHIR_MODE = --table
else
- MENHIR_MODE =
+ MENHIR_MODE =
endif
# Options.
@@ -68,7 +68,7 @@ ifeq ($(MENHIR_TABLE),true)
MENHIR_SUGGESTION = $(MENHIR) $(MENHIR_MODE) --suggest-comp-flags
- MENHIR_INCLUDES := $(shell \
+ MENHIR_INCLUDES ?= $(shell \
if $(MENHIR_SUGGESTION) | grep -e "-package" >/dev/null ; then \
echo "-I `ocamlfind query menhirLib`" ; \
else \
@@ -80,4 +80,3 @@ else
MENHIR_INCLUDES =
endif
-