diff options
| author | Théo Zimmermann | 2019-07-20 12:50:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-07-20 12:50:17 +0200 |
| commit | cd6fc50854285f02bf151e94bdfb819988531fd2 (patch) | |
| tree | 798fcfd6a0bd529a3d8ae8a25e1c1e62b728be26 /Makefile.common | |
| parent | c80dfb6bd8ff8625ced2cae8b6789707f904a118 (diff) | |
| parent | cf868740c3d18ee9ce9a6b38dd617784625a3cae (diff) | |
Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg files and insert it into .rst files
Ack-by: Zimmi48
Ack-by: gares
Ack-by: ppedrot
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) |