aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/PG-adapting.texi
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-29 14:39:36 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-29 14:39:36 +0000
commit37b12f273f13c263c484dca40c6d4be28b1d2d19 (patch)
tree5c8a61ebde9094610dbb36a82e09f99b1ff7687b /doc/PG-adapting.texi
parentf3b108308bad8b51d23685dabe79699238e4eceb (diff)
Remove proof-splash-extensions
Diffstat (limited to 'doc/PG-adapting.texi')
-rw-r--r--doc/PG-adapting.texi6
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