diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 5 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 1 | ||||
| -rw-r--r-- | doc/sphinx/dune | 7 |
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))) |