aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
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 018937fc6..d8c8ba4e8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -588,7 +588,7 @@ pluginsbyte: $(PLUGINS)
theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
$(SHOW)'COQC -noinit $<'
$(HIDE)rm -f theories/Init/$*.glob
- $(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq
+ $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq
theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
$(OCAML) $< $(TOTARGET)
@@ -1032,7 +1032,7 @@ plugins/%_mod.ml: plugins/%.mllib
%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
$(SHOW)'COQC $<'
$(HIDE)rm -f $*.glob
- $(HIDE)$(BOOTCOQC) $*
+ $(HIDE)$(BOOTCOQC) $<
ifdef VALIDATE
$(SHOW)'COQCHK $(call vo_to_mod,$@)'
$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \