aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--generic/proof-menu.el3
1 files changed, 2 insertions, 1 deletions
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 "-----")