Merge PR #9568: Add test that we regenerated doc/sphinx/README.rst to linter

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

3 files changed, 10 insertions, 3 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index e4f078c1d6..5861b18d2b 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -214,7 +214,7 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
 
     Example::
 
-       .. coqtop:: in reset undo
+       .. coqtop:: in undo
 
           Print nat.
           Definition a := 1.
@@ -234,8 +234,7 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
     - Behavior options
 
       - ``reset``: Send a ``Reset Initial`` command before running this block
-      - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
-        running all the commands in this block
+      - ``undo``: Reset state after executing. Not compatible with ``reset``.
 
     ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
     of the same document (``coqrst`` creates a single ``coqtop`` process per
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 9d2afc080f..48ad60c6dd 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -142,6 +142,7 @@ exclude_patterns = [
     'introduction.rst',
     'refman-preamble.rst',
     'README.rst',
+    'README.gen.rst',
     'README.template.rst'
 ] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS]
 
diff --git a/doc/sphinx/dune b/doc/sphinx/dune
index fff025c919..353d58c676 100644
--- a/doc/sphinx/dune
+++ b/doc/sphinx/dune
@@ -1 +1,8 @@
 (dirs :standard _static)
+
+(rule (targets README.gen.rst)
+ (deps (source_tree ../tools/coqrst) README.template.rst)
+ (action (run ../tools/coqrst/regen_readme.py %{targets})))
+
+(alias (name refman-html)
+  (action (diff README.rst README.gen.rst)))