From e8c5ac4646d162f82465193617885849c1c11969 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Mon, 5 Oct 1998 10:19:47 +0000
Subject: da> BTW, the menus have disappeared!

They are back courtesy of reintroducing an easy-menu-add call.
---
 generic/proof.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/generic/proof.el b/generic/proof.el
index ba095928..a0354cf9 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -2090,7 +2090,7 @@ finish setup which depends on specific proof assistant configuration."
   ;; calculate some strings and regexps for searching
   (setq proof-terminal-string (char-to-string proof-terminal-char))
 
-  ;; FIXME da: surely these are LEGO (Coq?) specific!
+  ;; FIXME: these are LEGO specific!
   (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string))
   (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string))
 
@@ -2143,6 +2143,7 @@ finish setup which depends on specific proof assistant configuration."
 		    proof-mode-map
 		    "Menu used in Proof General scripting mode."
 		    (cons proof-mode-name (cdr proof-menu)))
+  (easy-menu-add proof-mode-menu proof-mode-map)
 
   ;; For fontlock
   ;; FIXME (da): zap commas support is too specific, should be enabled
-- 
cgit v1.2.3