aboutsummaryrefslogtreecommitdiff
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 85bfb2e827..53acb99bf2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -542,9 +542,9 @@ $(GALLINA): $(GALLINACMO)
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ $(GALLINACMO)
-$(COQMAKEFILE): tools/coq_makefile.cmo
+$(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coq_makefile.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ config/coq_config.cmo tools/coq_makefile.cmo
$(COQTEX): tools/coq-tex.cmo
$(SHOW)'OCAMLC -o $@'