aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorMaxime Dénès2019-10-21 15:50:26 +0200
committerMaxime Dénès2019-10-21 15:50:26 +0200
commit50e3fd2b6f30ab209200950fd5a804a18b47288f (patch)
tree21085d5efc424c36d69963eab3fe123f0a261422 /Makefile.common
parentc6056bdc54d02dc5c6a91aeacb13460e8dd365e3 (diff)
parentcd03a27b917dedc129af980a6099b20134cba9f5 (diff)
Merge PR #10857: Fix votour after the change of representation of opaques.
Reviewed-by: SkySkimmer Reviewed-by: maximedenes
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index 2d1200c071..1ad255d156 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -41,9 +41,10 @@ COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py
COQTIME_FILE_MAKER:=tools/TimeFileMaker.py
COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
+VOTOUR:=bin/votour
TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
- $(COQWORKMGR) $(COQPP) $(DOC_GRAM)
+ $(COQWORKMGR) $(COQPP) $(DOC_GRAM) $(VOTOUR)
TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\
$(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES)