aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2001-03-20 17:38:23 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2001-03-20 17:38:23 +0000
commit67735f434627c4bfbc0bedd9a64bb824581efde7 (patch)
tree8c0b3f92edfecee44add1aad302bdc6194652748
parentb058e5209bf4968b9f31edcd4149251e659bbd6b (diff)
Updated magic
-rw-r--r--doc/PG-adapting.texi2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 5bbfb093..65576185 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1866,7 +1866,7 @@ Mark for goal.
This setting is also used to see if proof-by-pointing features
are configured. If it is unset, some of the code
-for parsing the is disabled.
+for parsing the prover output is disabled.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-field-char
@defvar proof-shell-field-char