diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2005-09-01 14:18:06 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2005-09-01 14:18:06 +0000 |
| commit | 93db85e34dae8006d1a0c6e5c5eea54d5ff2f12c (patch) | |
| tree | a8a20ec07c61477fe7498c6c38f0da72e93d5e0f | |
| parent | 1702b15d4aa280923592c749361f5344afb8ad68 (diff) | |
eager message: perform pg-remove-specials-in-string after pg-assoc-strip-subterm-markup;
| -rw-r--r-- | generic/proof-shell.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index ac05ba78..c2d59488 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1437,7 +1437,8 @@ MESSAGE should be a string annotated with ;; Don't bother remove the window for the response buffer ;; because we're about to put a message in it. (proof-shell-maybe-erase-response nil nil) - (let ((stripped (pg-assoc-strip-subterm-markup message))) + (let ((stripped (pg-remove-specials-in-string + (pg-assoc-strip-subterm-markup message)))) ;; Display first chunk of output in minibuffer. ;; Maybe this should be configurable, it can get noisy. (proof-shell-message |