From 433299f02dcc0ab055ee1447356a3b2c3d1f8d69 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 8 Jun 2003 20:31:03 +0000
Subject: Add insert last output onto menu

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

diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 44439ed0..d9992ff6 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -424,7 +424,8 @@ If in three window or multiple frame mode, display two buffers."
 	(append
 	 `(["Function Menu" function-menu
 	    ,menuvisiblep (fboundp 'function-menu)]
-	   ["Complete Identifier" proof-script-complete t])
+	   ["Complete Identifier" proof-script-complete t]
+	   ["Insert last output" pg-insert-last-output-as-comment proof-shell-last-output])
 	 (list "-----")
 	 proof-show-hide-menu
 	 (list "-----")
-- 
cgit v1.2.3