Merge PR #8191: [sphinx] Use arguments of '.. example::' directive as a title

1 files changed, 6 insertions, 2 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index c9487abf03..e6b71a8293 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -571,6 +571,9 @@ class ExampleDirective(BaseAdmonition):
     http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
     for more details.
 
+    Optionally, any text immediately following the ``.. example::`` header is
+    used as the example's title.
+
     Example::
 
        .. example:: Adding a hint to a database
@@ -583,13 +586,14 @@ class ExampleDirective(BaseAdmonition):
     """
     node_class = nodes.admonition
     directive_name = "example"
+    optional_arguments = 1
 
     def run(self):
         # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’,
         # and uses arguments[0] as the title in that case (in other cases, the
         # title is unset, and it is instead set in the HTML visitor).
-        assert not self.arguments # Arguments have been parsed as content
-        self.arguments = ['Example']
+        assert len(self.arguments) <= 1
+        self.arguments = [": ".join(['Example'] + self.arguments)]
         self.options['classes'] = ['admonition', 'note']
         return super().run()