aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-12 18:48:28 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-12 19:33:43 +0200
commit1419bb9ddd1299673707404f1f35b4904648760b (patch)
treea6715760d7536a29d13c9d06b116b36c1bee4a95 /Makefile.dev
parente99a1fa8d225496e2a5f74d1247a99a07dba4597 (diff)
[dev] Autogenerate OCaml dev files.
For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev18
1 files changed, 16 insertions, 2 deletions
diff --git a/Makefile.dev b/Makefile.dev
index 8f7d21694..59097bd91 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -15,7 +15,7 @@
# Debug printers in dev/
#########################
-.PHONY: devel printers
+.PHONY: devel printers camldevfiles
DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo
@@ -85,13 +85,27 @@ endif
# But these partial targets could be quite handy for quick builds
# of specific components of Coq.
+###########################################################################
+# OCaml dev files
+###########################################################################
+camldevfiles: $(MERLINFILES) META.coq
+
+.merlin: .merlin.in
+ cp -a "$<" "$@"
+
+%/.merlin: %/.merlin.in
+ cp -a "$<" "$@"
+
+META.coq: META.coq.in
+ cp -a "$<" "$@"
+
###############################
### 1) general-purpose targets
###############################
coqlight: theories-light tools coqbinaries
-states: theories/Init/Prelude.vo
+states: camldevfiles theories/Init/Prelude.vo
miniopt: $(COQTOPEXE) pluginsopt
minibyte: $(COQTOPBYTE) pluginsbyte