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