aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2003-05-24 11:13:37 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2003-05-24 11:13:37 +0000
commit65b0b3f8afe365e726741b556be49eb016d0b78e (patch)
tree2aedbb58feccec9cb5ea99b3276dffad6ef5e528 /generic
parent88dca363e3d7b17217b097997b0ec96344e3bea1 (diff)
Add hint triggered when processing complete
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-shell.el3
1 files changed, 3 insertions, 0 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 87cf6d5c..7589ead4 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1108,6 +1108,9 @@ The return value is non-nil if the action list is now empty."
(if (null proof-action-list)
(progn (proof-release-lock)
(proof-detach-queue)
+ ;; give a hint to the user in case we've finished
+ ;; a batch of input
+ (pg-processing-complete-hint)
;; indicate finished
t)
;; Otherwise, send the next command to the process.