diff options
Diffstat (limited to 'generic/pg-response.el')
| -rw-r--r-- | generic/pg-response.el | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/generic/pg-response.el b/generic/pg-response.el index 34e7ba08..75fb8fdd 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -144,8 +144,11 @@ Returns non-nil if response buffer was cleared." (unless pg-use-specials-for-fontify (setq str (pg-assoc-strip-subterm-markup str))) (proof-shell-maybe-erase-response t nil) - (pg-response-display-with-face str) - (proof-display-and-keep-buffer proof-response-buffer)) + (unless (or (string-equal str "") (string-equal str "\n")) + ;; don't display an empty buffer [ NB: above test repeated below, + ;; but response-display reused elsewhere ] + (pg-response-display-with-face str) + (proof-display-and-keep-buffer proof-response-buffer))) ;; FIXME: this function should be combined with ;; proof-shell-maybe-erase-response-buffer. |