aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-03-01 21:21:09 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-03-02 20:00:03 +0100
commitf694544d016b085b3cd10007b9f7716ae2c3b022 (patch)
tree36a6dd3389db0151edc798d7aa91e95b6ea0b151 /Makefile
parent761316ea73ad23be898470caa1a7bf839fa4a12e (diff)
Makefile: the initial build of grammar.cma is now directory-driven
In last commit, we used grep to decide whether a .ml4 could be compiled during the initial phase of not. Instead, we now rely on a simpler directory dichotomy: - config lib kernel library pretyping interp parsing grammar are considered initial (and shouldn't contain grammar-dependent .ml4), see $(GRAMSRCDIRS) in Makefile.common - the grammar-dependent .ml4 could be in any other directories Currently, they are in: tactics toplevel plugins/*
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile9
1 files changed, 0 insertions, 9 deletions
diff --git a/Makefile b/Makefile
index 5f5397fa7..109196bea 100644
--- a/Makefile
+++ b/Makefile
@@ -59,20 +59,11 @@ define find
$(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
endef
-define findx
- $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
-endef
-
-# We now discriminate .ml4 files according to their need of grammar.cma
-# or q_constr.cmo
-USEGRAMMAR := '(\*.*camlp4deps.*grammar'
-
## Files in the source tree
YACCFILES:=$(call find, '*.mly')
LEXFILES := $(call find, '*.mll')
export MLLIBFILES := $(call find, '*.mllib')
-export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR))
export ML4FILES := $(call find, '*.ml4')
export CFILES := $(call find, '*.c')