diff options
| author | Jim Fehrle | 2020-04-01 13:18:03 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-06-08 16:50:53 -0700 |
| commit | 27d6686f399f40904ff6005a84677907d53c5bbf (patch) | |
| tree | 5a27b8acdab8ce79b9a7d10685c8979cda82416b /Makefile.doc | |
| parent | 6a76e4394876cb08b02d8e7ea185049147f9cd2b (diff) | |
Convert Ltac chapter to prodn
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.doc b/Makefile.doc index 3dc627abdf..cc6277ca79 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -248,7 +248,8 @@ $(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/too # user-contrib/*/*.mlg omitted for now (e.g. ltac2) PLUGIN_MLGS := $(wildcard plugins/*/*.mlg) -OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg +OMITTED_PLUGIN_MLGS := plugins/ssr/ssrparser.mlg plugins/ssr/ssrvernac.mlg plugins/ssrmatching/g_ssrmatching.mlg \ + plugins/ssrsearch/g_search.mlg DOC_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg) DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) $(wildcard doc/sphinx/*/*/*.rst) @@ -260,7 +261,7 @@ doc/tools/docgram/fullGrammar: $(DOC_GRAM) $(DOC_MLGS) #todo: add a dependency of sphinx on updated_rsts when we're ready doc/tools/docgram/orderedGrammar doc/tools/docgram/updated_rsts: doc/tools/docgram/fullGrammar $(DOC_GRAM) $(DOC_EDIT_MLGS) $(SHOW)'DOC_GRAM_RSTS' - $(HIDE)$(DOC_GRAM) -check-cmds $(DOC_MLGS) $(DOC_RSTS) + $(HIDE)$(DOC_GRAM) -check-cmds -check-tacs $(DOC_MLGS) $(DOC_RSTS) doc/tools/docgram/updated_rsts: doc/tools/docgram/orderedGrammar |