From 20f916a79c8053fee8c416827cc28ac77ea994c5 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 10 Mar 2000 05:54:52 +0000
Subject: Use name of proof assistant in menu.

---
 generic/proof-script.el | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/generic/proof-script.el b/generic/proof-script.el
index ce97d623..6fffb0bc 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2296,12 +2296,14 @@ This is intended as a value for proof-activate-scripting-hook"
 (defvar proof-shared-menu
   (append
     (list
-     ["Start proof assistant"
-      proof-shell-start
-      :active (not (proof-shell-live-buffer))]
-     ["Exit proof assistant"
-      proof-shell-exit
-      :active (proof-shell-live-buffer)])
+     (vector
+      (concat "Start " proof-assistant)
+      'proof-shell-start
+      ':active '(not (proof-shell-live-buffer)))
+     (vector
+      (concat "Exit " proof-assistant)
+      'proof-shell-exit
+      ':active '(proof-shell-live-buffer)))
     (list proof-buffer-menu)
     (list proof-quick-opts-menu)
     (list proof-help-menu))
-- 
cgit v1.2.3