aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-18 16:19:35 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-18 16:19:35 +0000
commit14546c942f950b11e1afee9fec396eb21889b75d (patch)
treee1ed119c7c6650fed7c5753d8ed39a729b2ffe62
parentb087d7665e87d333d6e85ec92b9f161e0368c528 (diff)
proof-autosend-loop: don't enter if shell is already busy processing
-rw-r--r--generic/pg-user.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 66e3a979..d884594c 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1434,7 +1434,8 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
(defun proof-autosend-loop ()
(proof-with-current-buffer-if-exists proof-script-buffer
- (unless (proof-locked-region-full-p)
+ (unless (or (proof-locked-region-full-p)
+ proof-shell-busy)
(proof-autosend-loop-all))))
(defun proof-autosend-loop-all ()