diff options
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index d884594c..60ba77b1 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -194,8 +194,11 @@ If inside a comment, just process until the start of the comment." (save-excursion (goto-char (point-max)) (proof-assert-until-point-interactive)) - (proof-maybe-follow-locked-end))) - + (proof-maybe-follow-locked-end)) + (when proof-fast-process-buffer + (message "Processing buffer...") + (proof-shell-wait) + (message "Processing buffer...done"))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |