From 1ae6589f077f76de8d279ac5fc5d4301792ba51e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 30 Aug 2001 14:18:16 +0000
Subject: pg-insert-last-output-as-comment strips special annotations from last
 output before inserting as comment.

---
 generic/pg-user.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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))))))
     
   
-- 
cgit v1.2.3