diff options
| author | Jim Fehrle | 2020-06-23 14:06:50 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-07-08 11:36:27 -0700 |
| commit | fa3d479cbf3f84a231fe8587c321df03538b18e7 (patch) | |
| tree | 8e1beffb2922635ab6546014a4559a2989c0b3f4 /Makefile.doc | |
| parent | b291704713f762cf93e5fda012f297ddd895b5fd (diff) | |
Add tags in prodn indicating productions that are from plugins,
filtered-only show Ltac2 tags outside of ltac2.rst
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 cc6277ca79..473a70fb72 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -223,7 +223,7 @@ install-doc-stdlib-html: $(MKDIR) $(FULLDOCDIR)/html/stdlib $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib -install-doc-printable: +install-doc-printable: $(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps @@ -250,7 +250,8 @@ $(DOC_GRAM): $(DOC_GRAMCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml doc/too PLUGIN_MLGS := $(wildcard plugins/*/*.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_MLGS := $(wildcard */*.mlg) $(sort $(filter-out $(OMITTED_PLUGIN_MLGS), $(PLUGIN_MLGS))) \ + user-contrib/Ltac2/g_ltac2.mlg DOC_EDIT_MLGS := $(wildcard doc/tools/docgram/*.edit_mlg) DOC_RSTS := $(wildcard doc/sphinx/*/*.rst) $(wildcard doc/sphinx/*/*/*.rst) |