diff options
author | 2001-08-30 14:37:59 +0000 | |
---|---|---|
committer | 2001-08-30 14:37:59 +0000 | |
commit | 607a970309d0fdb47e0ac3df2f49cd6d59731861 (patch) | |
tree | f2c167c82d356dc702404f9190d7842682d37027 /generic/proof-shell.el | |
parent | f7b368627c7e754aa916b07e8c996ea6559dcfc4 (diff) |
Add reassurance to interrupt warning to make Markus happier.
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r-- | generic/proof-shell.el | 3 |
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) |