diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2001-08-30 14:18:16 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2001-08-30 14:18:16 +0000 |
| commit | 1ae6589f077f76de8d279ac5fc5d4301792ba51e (patch) | |
| tree | 8a27d714d9ce5df67e0b69b9caa5534fd8010446 | |
| parent | a1acb2a34bb28aaaa4270cd5ebda7fcad52cb897 (diff) | |
pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment.
| -rw-r--r-- | generic/pg-user.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index e3317f9b..0750acbc 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -680,7 +680,8 @@ last use time, to discourage saving these into the users database." (pg-insert-output-as-comment-fn proof-shell-last-output) ;; Otherwise the default behaviour is to use comment-region (let ((beg (point))) - (insert proof-shell-last-output) + (insert (proof-shell-strip-special-annotations + proof-shell-last-output)) (comment-region beg (point)))))) |