diff options
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 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) |