aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile53
1 files changed, 18 insertions, 35 deletions
diff --git a/Makefile b/Makefile
index 38be3013d..4787377ea 100644
--- a/Makefile
+++ b/Makefile
@@ -78,6 +78,7 @@ export MLLIBFILES := $(call find, '*.mllib')
export MLPACKFILES := $(call find, '*.mlpack')
export ML4FILES := $(call find, '*.ml4')
export CFILES := $(call findindir, 'kernel/byterun', '*.c')
+export MERLINFILES := $(call find, '.merlin')
# NB: The lists of currently existing .ml and .mli files will change
# before and after a build or a make clean. Hence we do not export
@@ -137,40 +138,6 @@ Then, you may want to consider whether you want to restore the autosaves)
#run.
endif
-# Check that every compiled file around has a known source file.
-# This should help preventing weird compilation failures caused by leftover
-# compiled files after deleting or moving some source files.
-
-EXISTINGVO:=$(call find, '*.vo')
-KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
-ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))
-
-EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
-KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \
- $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
-KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
- $(MLIFILES:.mli=.cmi) \
- $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
-ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS))
-
-ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii
-ifndef ACCEPT_ALIEN_VO
-ifdef ALIENVO
-$(error Leftover compiled Coq files without known sources: $(ALIENVO); \
-remove them first, for instance via 'make voclean' or 'make alienclean' \
-(or skip this check via 'make ACCEPT_ALIEN_VO=1'))
-endif
-endif
-
-ifndef ACCEPT_ALIEN_OBJ
-ifdef ALIENOBJS
-$(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \
-remove them first, for instance via 'make clean' or 'make alienclean' \
-(or skip this check via 'make ACCEPT_ALIEN_OBJ=1'))
-endif
-endif
-endif
-
# Apart from clean and tags, everything will be done in a sub-call to make
# on Makefile.build. This way, we avoid doing here the -include of .d :
# since they trigger some compilations, we do not want them for a mere clean.
@@ -186,7 +153,7 @@ endif
MAKE_OPTS := --warn-undefined-variable --no-builtin-rules
-submake:
+submake: alienclean
$(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)
noconfig:
@@ -282,6 +249,22 @@ devdocclean:
rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex
rm -f $(OCAMLDOCDIR)/html/*.html
+# Ensure that every compiled file around has a known source file.
+# This should help preventing weird compilation failures caused by leftover
+# compiled files after deleting or moving some source files.
+
+EXISTINGVO:=$(call find, '*.vo')
+KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
+ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))
+
+EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
+KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \
+ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
+KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
+ $(MLIFILES:.mli=.cmi) \
+ $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
+ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS))
+
alienclean:
rm -f $(ALIENOBJS) $(ALIENVO)