diff options
author | 2007-12-14 10:38:55 +0000 | |
---|---|---|
committer | 2007-12-14 10:38:55 +0000 | |
commit | a8e8ffa54ac578e5657853bd163c5b09a313f178 (patch) | |
tree | 45c798555c2f7ccbc8a744ef56ca88cf06cbba17 /generic/pg-response.el | |
parent | f60e5be1803cd30f9030a1a432d8a64561882f35 (diff) |
Use proof-shell-unicode to control whether bytes 128-255 are stripped from output.
Diffstat (limited to 'generic/pg-response.el')
-rw-r--r-- | generic/pg-response.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/pg-response.el b/generic/pg-response.el index 015b111a..a1058f18 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -275,7 +275,8 @@ Returns non-nil if response buffer was cleared." (defun pg-response-display (str) "Show STR as a response in the response buffer." - (unless pg-use-specials-for-fontify + (unless (or proof-shell-unicode + pg-use-specials-for-fontify) (setq str (pg-assoc-strip-subterm-markup str))) (proof-shell-maybe-erase-response t nil) ;;(unless (or (string-equal str "") (string-equal str "\n")) |