aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-08-28 13:03:43 +0200
committerGaëtan Gilbert2018-08-28 13:03:43 +0200
commit35c28d8c506e1bb4d9b2f2afa6f2702aa359dc13 (patch)
tree204a2458b21dca908a34e625c6cefa711c053703 /Makefile
parentf885e8a88620351d9dc4b0969f520d13197f2184 (diff)
Put camldevfiles targets in Makefile
There's no need to build dependencies for it.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile33
1 files changed, 24 insertions, 9 deletions
diff --git a/Makefile b/Makefile
index 636093d7a5..344f2ee972 100644
--- a/Makefile
+++ b/Makefile
@@ -81,7 +81,7 @@ export ML4FILES := $(call find, '*.ml4')
export MLGFILES := $(call find, '*.mlg')
export CFILES := $(call findindir, 'kernel/byterun', '*.c')
-export MERLININFILES := $(call find, '.merlin.in')
+MERLININFILES := $(call find, '.merlin.in')
export MERLINFILES := $(MERLININFILES:.in=)
# NB: The lists of currently existing .ml and .mli files will change
@@ -116,7 +116,7 @@ include Makefile.common
NOARG: world
-.PHONY: NOARG help noconfig submake
+.PHONY: NOARG help noconfig submake camldevfiles
help:
@echo "Please use either:"
@@ -143,12 +143,13 @@ Then, you may want to consider whether you want to restore the autosaves)
#run.
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.
-# Moreover, we regroup this sub-call in a common target named 'submake'.
-# This way, multiple user-given goals (cf the MAKECMDGOALS variable) won't
-# trigger multiple (possibly parallel) make sub-calls
+# Apart from clean and a few misc files, 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. Moreover, we regroup this sub-call in a
+# common target named 'submake'. This way, multiple user-given goals
+# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly
+# parallel) make sub-calls
ifdef COQ_CONFIGURED
%:: submake ;
@@ -161,7 +162,7 @@ MAKE_OPTS := --warn-undefined-variable --no-builtin-rules
bin:
mkdir bin
-submake: alienclean | bin
+submake: alienclean camldevfiles | bin
$(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)
noconfig:
@@ -172,6 +173,20 @@ noconfig:
Makefile $(wildcard Makefile.*) config/Makefile : ;
###########################################################################
+# OCaml dev files
+###########################################################################
+camldevfiles: $(MERLINFILES) META.coq
+
+.merlin: .merlin.in
+ cp -a "$<" "$@"
+
+%/.merlin: %/.merlin.in
+ cp -a "$<" "$@"
+
+META.coq: META.coq.in
+ cp -a "$<" "$@"
+
+###########################################################################
# Cleaning
###########################################################################