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/proof-engine/ltac.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/proof-engine')

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