diff options
| author | Pierre-Marie Pédrot | 2019-10-09 10:38:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-18 20:15:27 +0200 |
| commit | cd03a27b917dedc129af980a6099b20134cba9f5 (patch) | |
| tree | df60a9c4615067c39fad99e6e1cb05a427eb4b2a /Makefile.common | |
| parent | 3e5a44e099d3fe847693887a09b57dfb4e2349e8 (diff) | |
Adding a test for votour.
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 3 |
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) |