From e9ac9e8eb3d2567ff1ab12cf7bfdd60d5df2c30f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 1 May 2000 18:18:30 +0000
Subject: Added proof-assistant-menu-entries for proof assistant specific
 menus.

---
 doc/ProofGeneral.texi | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 0083a54c..b2995081 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3534,6 +3534,19 @@ The following variables should be set in the script mode before
 @code{proof-config-done} is called.  These make some settings for the
 commands and menus available in Proof General.
 
+The first setting controls the proof-assistant specific menu,
+if any is defined.
+
+@c TEXI DOCSTRING MAGIC: proof-assistant-menu-entries
+@defvar proof-assistant-menu-entries 
+Entries for proof assistant specific menu. @*
+A list of menu items [@var{name} @var{callback} ENABLE].  See the documentation
+of @samp{@code{easy-menu-define}} for more details.
+@end defvar
+
+The remaining settings control the standard commands available
+from the generic menu and the toolbar.
+
 @c TEXI DOCSTRING MAGIC: proof-assistant-home-page
 @defvar proof-assistant-home-page 
 Web address for information on proof assistant.@*
@@ -3576,6 +3589,8 @@ If a function, it should return the command string to insert.
 
 
 
+
+
 @c defgroup proof-script
 @node Proof script settings
 @section Proof script settings
-- 
cgit v1.2.3