diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-01 10:24:22 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-01 10:24:22 +0000 |
| commit | 57f530aad7a13ddd08c61aa3a514732361b599f9 (patch) | |
| tree | 65f2b3ef53ee985754addcfb119ed774a18ecb21 /generic/proof-shell.el | |
| parent | e37e00a0a116f66bbc122b8991daa9f909f7bb05 (diff) | |
Fix bug for proof-shell-leave-annotations-in-output.
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 141a61d6..274d05f8 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -729,8 +729,9 @@ Returns the string (with faces) in the specified region." (setq start (search-backward-regexp start-regexp)) (setq end (- (search-forward-regexp end-regexp) (length (match-string 0)))) - (unless proof-shell-leave-annotations-in-output - (setq string + (setq string + (if proof-shell-leave-annotations-in-output + (buffer-substring start end) (proof-shell-strip-special-annotations (buffer-substring start end))))) ;; Erase if need be, and erase next time round too. |