From 897f975d7ac0efde149a8647afe46c7706355c5a Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 22 Sep 1999 17:08:38 +0000
Subject: Docstrings

---
 generic/proof-config.el | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 1f85a377..13f0e3ee 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -824,19 +824,21 @@ will be lost.
 
 The engine matches interrupts before errors, see proof-shell-interupt-regexp.
 
-It is safe to leave this variable unset nil."
+It is safe to leave this variable unset (as nil)."
   :type '(choice nil regexp)
   :group 'proof-shell) 
 
 (defcustom proof-shell-interrupt-regexp nil
   "Regexp matching output indicating the assistant was interrupted.
-We assume that an interrupt message corresponds to a failure
-in the last proof command executed. So don't match
-mere warning messages with this regexp.
-Moreover, an interrupt message should not be matched as
-an eager annotation (see proof-shell-eager-annotation-start)
-otherwise it will be lost.
-The engine matches interrupts before errors."
+We assume that an error message corresponds to a failure in the last
+proof command executed.  So don't match mere warning messages with
+this regexp.  Moreover, an error message should not be matched as an
+eager annotation (see proof-shell-eager-annotation-start) otherwise it
+will be lost.
+
+The engine matches interrupts before errors, see proof-shell-error-regexp.
+
+It is safe to leave this variable unset (as nil)."
   :type 'regexp
   :group 'proof-shell) 
 
-- 
cgit v1.2.3