diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 16:19:35 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 16:19:35 +0000 |
commit | 14546c942f950b11e1afee9fec396eb21889b75d (patch) | |
tree | e1ed119c7c6650fed7c5753d8ed39a729b2ffe62 | |
parent | b087d7665e87d333d6e85ec92b9f161e0368c528 (diff) |
proof-autosend-loop: don't enter if shell is already busy processing
-rw-r--r-- | generic/pg-user.el | 3 |
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 () |