aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-01-15 17:49:49 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-01-15 17:49:49 +0100
commit74a5cfa8b2f1a881ebf010160421cf0775c2a084 (patch)
tree60444d73bc9f0824920b34d60b60b6721a603e92 /Makefile.build
parent088977e086a5fd72f5f724192e5cb5ba1a0d9bb6 (diff)
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index 032f46508..48f448ce8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -587,9 +587,9 @@ pluginsbyte: $(PLUGINS)
###########################################################################
theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
- $(SHOW)'COQC -noinit $<'
+ $(SHOW)'COQC $(COQ_XML) -noinit $<'
$(HIDE)rm -f theories/Init/$*.glob
- $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq
+ $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
$(OCAML) $< $(TOTARGET)