diff options
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 2 |
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) |