From cd03a27b917dedc129af980a6099b20134cba9f5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 9 Oct 2019 10:38:51 +0200
Subject: Adding a test for votour.

---
 Makefile.common | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Makefile.common')

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)
 
-- 
cgit v1.2.3