From fa3d479cbf3f84a231fe8587c321df03538b18e7 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 23 Jun 2020 14:06:50 -0700
Subject: Add tags in prodn indicating productions that are from plugins,
 filtered-only show Ltac2 tags outside of ltac2.rst

---
 Makefile.doc | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Makefile.doc')

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)
 
-- 
cgit v1.2.3