diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-31 12:14:55 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 00:53:49 +0200 |
commit | d0a9edabf59a858625d11516cdb230d223a77aeb (patch) | |
tree | b5b416167824a209b8842e41d6bed19bc57f2a19 /Makefile | |
parent | 1532e4d57fce07e8a1cd6838853a4a31ea84e453 (diff) |
Yet another Makefile reform : a unique phase without nasty make tricks
We're back to a unique build phase (as before e372b72), but without
relying on the awkward include-deps-failed-lets-retry feature of make.
Since PMP has made grammar/ self-contained, we could now build
grammar.cma in a rather straightforward way, no need for
a specific sub-call to $(MAKE) for that. The dependencies between
files of grammar/ are stated explicitely, since .d files aren't
fully available initially.
Some Makefile simplifications, for instance remove the CAMLP4DEPS
shell horror. Instead, we generalize the use of two different
filename extensions :
- a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
- a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
except coqide_main.ml4 and its specific rule
Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
.ml4 dichotomy)
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 8 |
1 files changed, 0 insertions, 8 deletions
@@ -63,15 +63,10 @@ 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 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') @@ -150,10 +145,7 @@ endif MAKE_OPTS := --warn-undefined-variable --no-builtin-rules -GRAM_TARGETS := grammar/grammar.cma grammar/q_constr.cmo - submake: - $(MAKE) $(MAKE_OPTS) -f Makefile.build BUILDGRAMMAR=1 $(GRAM_TARGETS) $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) noconfig: |