From cf868740c3d18ee9ce9a6b38dd617784625a3cae Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 9 Jan 2019 15:32:52 -0800
Subject: Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg
 files and inserting it into the .rst files

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

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index b331484fb2..dd23d7dd2f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -22,6 +22,7 @@ COQTOPBYTE:=bin/coqtop.byte$(EXE)
 
 COQDEP:=bin/coqdep$(EXE)
 COQPP:=bin/coqpp$(EXE)
+DOC_GRAM:=bin/doc_grammar$(EXE)
 COQDEPBYTE:=bin/coqdep.byte$(EXE)
 COQMAKEFILE:=bin/coq_makefile$(EXE)
 COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE)
@@ -42,7 +43,7 @@ COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
 COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
 
 TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
-	$(COQWORKMGR) $(COQPP)
+	$(COQWORKMGR) $(COQPP) $(DOC_GRAM)
 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