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

---
 doc/sphinx/_static/notations.css | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/_static/notations.css')

diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 9546f7107e..8c3f7ac3c1 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -192,7 +192,8 @@
 
 .prodn-cell-nonterminal,
 .prodn-cell-op,
-.prodn-cell-production
+.prodn-cell-production,
+.prodn-cell-tag
 {
     display: table-cell;
 }
@@ -206,6 +207,17 @@
     font-weight: normal;
 }
 
+.prodn-cell-production {
+    width: 99%;
+}
+
+.prodn-cell-tag {
+    text-align: right;
+    font-weight: normal;
+    font-size: 75%;
+    font-family: "Lato","proxima-nova","Helvetica Neue",Arial,sans-serif;
+}
+
 .prodn-table .notation > .repeat-wrapper {
     margin-top: 0.28em;
 }
-- 
cgit v1.2.3