From f3db5a4006a3da598c4aa76adcf26729305b8dc5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 14:19:28 +0100
Subject: Sphinx: fail when a command fails

This uses a new coqtop-only option "Coqtop Exit On Error", not sure where
to put the doc for it. It being an option means we can locally turn it
off (.. coqtop:: fail).
---
 doc/sphinx/README.rst                       | 1 +
 doc/sphinx/practical-tools/coq-commands.rst | 5 +++++
 doc/sphinx/proof-engine/ltac.rst            | 2 +-
 3 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 4f61824e67..a341cd9401 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -234,6 +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
+      - ``fail``: Don't die if a command fails.
 
     ``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/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 1b4d2315aa..eebf1f11e1 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -34,6 +34,11 @@ allow dynamic linking of tactics). You can switch to the OCaml toplevel
 with the command ``Drop.``, and come back to the |Coq|
 toplevel with the command ``Coqloop.loop();;``.
 
+.. flag:: Coqtop Exit On Error
+
+   This option, off by default, causes coqtop to exit with status code
+   ``1`` if a command produces an error instead of recovering from it.
+
 Batch compilation (coqc)
 ------------------------
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c134563efe..c1da1112c8 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -602,7 +602,7 @@ Failing
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: all fail
 
          Goal True.
          Proof. fail. Abort.
-- 
cgit v1.2.3