From 6e079495ba13341261c3f7e3604b1a6b7db6ecc9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 25 Aug 2010 09:36:43 +0000
Subject: proof-shell-handle-error-or-interrupt: prevent an error in an obscure
 case, attempting to handle delayed output when there is none.

---
 generic/proof-shell.el | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'generic')

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 0c738696..e80bdf0b 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -573,8 +573,9 @@ didn't cause prover output."
        "Interrupt: script management may be in an inconsistent state
 	   (but it's probably okay)"))
      (t ; error
-      (save-excursion
-	(proof-shell-handle-delayed-output))
+      (if proof-shell-delayed-output-start 
+	  (save-excursion
+	    (proof-shell-handle-delayed-output)))
       (proof-shell-handle-error-output
        (if proof-shell-truncate-before-error proof-shell-error-regexp)
        'proof-error-face)
-- 
cgit v1.2.3