diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.common | 3 | ||||
| -rw-r--r-- | configure.ml | 2 | ||||
| -rwxr-xr-x | test-suite/misc/votour.sh | 3 |
4 files changed, 7 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 35f5e26272..ed4cde2b16 100644 --- a/Makefile.build +++ b/Makefile.build @@ -81,7 +81,7 @@ coq.timing.diff: coqlib.timing.diff # shouldn't be done in a same make -j... run, otherwise both ocamlc and # ocamlopt might race for access to the same .cmi files. -byte: coqbyte coqide-byte pluginsbyte printers +byte: coqbyte coqide-byte pluginsbyte printers bin/votour.byte .PHONY: world coq byte world.timing.diff coq.timing.diff 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) diff --git a/configure.ml b/configure.ml index e59a41a8d4..8e04dc46b2 100644 --- a/configure.ml +++ b/configure.ml @@ -20,7 +20,7 @@ let state_magic = 581091 let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; - "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"] + "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep";"votour"] let verbose = ref false (* for debugging this script *) diff --git a/test-suite/misc/votour.sh b/test-suite/misc/votour.sh new file mode 100755 index 0000000000..ac26aed49b --- /dev/null +++ b/test-suite/misc/votour.sh @@ -0,0 +1,3 @@ +command -v "${BIN}votour" || { echo "Missing votour"; exit 1; } + +"${BIN}votour" prerequisite/ssr_mini_mathcomp.vo < /dev/null |