diff options
| -rw-r--r-- | doc/PG-adapting.texi | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index ca998d1c..5144d426 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2005,6 +2005,7 @@ The splash screen may be displayed for a couple of seconds longer than this, depending on how long it takes the machine to initialise Proof General. @end defvar + @c TEXI DOCSTRING MAGIC: proof-splash-contents @defvar proof-splash-contents Evaluated to configure splash screen displayed when entering Proof General.@* @@ -2012,11 +2013,6 @@ A list of the screen contents. If an element is a string or an image specifier, it is displayed centred on the window on its own line. If it is nil, a new line is inserted. @end defvar -@c TEXI DOCSTRING MAGIC: proof-splash-extensions -@defvar proof-splash-extensions -Prover specific extensions of splash screen.@* -These are evaluated and appended to @samp{@code{proof-splash-contents}}. -@end defvar |