aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-shell.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2001-08-30 14:37:59 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2001-08-30 14:37:59 +0000
commit607a970309d0fdb47e0ac3df2f49cd6d59731861 (patch)
treef2c167c82d356dc702404f9190d7842682d37027 /generic/proof-shell.el
parentf7b368627c7e754aa916b07e8c996ea6559dcfc4 (diff)
Add reassurance to interrupt warning to make Markus happier.
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r--generic/proof-shell.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 94bee243..9fd176ab 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -834,7 +834,8 @@ Then we call `proof-shell-error-or-interrupt-action', which see."
'proof-error-face)
; (proof-display-and-keep-buffer proof-response-buffer)
(proof-warning
- "Interrupt: script management may be in an inconsistent state")
+ "Interrupt: script management may be in an inconsistent state
+ (but it's probably okay)")
(proof-shell-error-or-interrupt-action 'interrupt))
(defun proof-shell-error-or-interrupt-action (&optional err-or-int)