diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-06-08 20:31:03 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-06-08 20:31:03 +0000 |
| commit | 433299f02dcc0ab055ee1447356a3b2c3d1f8d69 (patch) | |
| tree | 80e68a4bf5e1a956754264e6a0e899441e6070ed | |
| parent | bc447583fd85d770bc676162c7b124bbfbe9b84e (diff) | |
Add insert last output onto menu
| -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 "-----") |