diff options
-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)))))) |