From e266976abc8c170c1e4bf1c98629c190b844f1ab Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel <clement.pitclaudel@live.com>
Date: Sat, 5 May 2018 12:25:46 -0400
Subject: [doc] More feedback on doc writer guide

Co-Authored-By: @Zimmi48
---
 doc/tools/coqrst/coqdomain.py | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index f8bb113a7..606d725bf 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -829,8 +829,7 @@ class IndexXRefRole(XRefRole):
         return title, target
 
 def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
-    """A Sphinx role to format grammar productions not included in a
-    `productionlist` directive.
+    """A grammar production not included in a ``productionlist`` directive.
 
     Useful to informally introduce a production, as part of running text.
 
-- 
cgit v1.2.3