diff options
author | 2002-08-07 10:09:40 +0000 | |
---|---|---|
committer | 2002-08-07 10:09:40 +0000 | |
commit | cdd4c5d78b0ef792ae6d43f98a54b8813bcfb5fa (patch) | |
tree | adf9db6ec35912883da36ddc25aaa78ca62a626e /generic/pg-response.el | |
parent | e2ac74a6bcca223394d2db5399394ef0fd445c77 (diff) |
Reorganized menus; add options save function; fix capitalization of names
Diffstat (limited to 'generic/pg-response.el')
-rw-r--r-- | generic/pg-response.el | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/generic/pg-response.el b/generic/pg-response.el index c1220a53..65fe9343 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -36,12 +36,7 @@ (easy-menu-define proof-response-mode-menu proof-response-mode-map "Menu for Proof General response buffer." - (cons proof-general-name - (append - proof-toolbar-scripting-menu - proof-shared-menu - proof-config-menu - proof-bug-report-menu))) + proof-aux-menu) (defun proof-response-config-done () |