aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-shell.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2012-11-09 13:43:39 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2012-11-09 13:43:39 +0000
commit40011e8fc1d6eafcc7dc9b1c43e22afbaeb98d6f (patch)
tree9007f72d34eaba62594dbf00729d050ba2aead7d /generic/proof-shell.el
parentd0774112051c18933eb75799e749e726d8f87efc (diff)
Doc for pg-finish-tracing-display
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r--generic/proof-shell.el2
1 files changed, 2 insertions, 0 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f64b110e..2e44c3cc 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1614,6 +1614,8 @@ Only works when system timer has microsecond count available."
(setq pg-tracing-slow-mode dontprint)))
(defun pg-finish-tracing-display ()
+ "Handle the end of possibly voluminous tracing-style output.
+If the output update was slowed down, show it now."
(proof-trace-buffer-finish)
(when pg-tracing-slow-mode
(proof-display-and-keep-buffer proof-trace-buffer)