diff options
-rw-r--r-- | generic/proof-menu.el | 3 |
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 "-----") |