aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-goals.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-07 10:09:40 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-07 10:09:40 +0000
commitcdd4c5d78b0ef792ae6d43f98a54b8813bcfb5fa (patch)
treeadf9db6ec35912883da36ddc25aaa78ca62a626e /generic/pg-goals.el
parente2ac74a6bcca223394d2db5399394ef0fd445c77 (diff)
Reorganized menus; add options save function; fix capitalization of names
Diffstat (limited to 'generic/pg-goals.el')
-rw-r--r--generic/pg-goals.el9
1 files changed, 2 insertions, 7 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index e28ef1cd..f3ac36df 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -49,17 +49,12 @@ May enable proof-by-pointing or similar features.
;;
-;; Menu for goals buffer (identical to response mode menu currently)
+;; Menu for goals buffer
;;
(easy-menu-define proof-goals-mode-menu
proof-goals-mode-map
"Menu for Proof General goals 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-goals-config-done ()
"Initialise the goals buffer after the child has been configured."