aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-10-02 17:47:33 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-10-02 17:47:33 +0000
commit781e80c6a69cac7b991207fae312a305d8ff6a55 (patch)
treefb945570ec5ed8543515054d619dc94914a7a2b8
parentffc8dbe7f626581b60a32c53a6ccc5b14b88279f (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 f97e76a3..057d4ad7 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -775,7 +775,7 @@ but you can set this variable to something else more precise if necessary.
@c TEXI DOCSTRING MAGIC: proof-comment-end
@defvar proof-comment-end
String which ends a comment in the proof assistant command language.@*
-The script buffer's @code{comment-end} is set to this string plus a space.
+The script buffer's @code{comment-end} is set to a space plus this string.
See also @samp{@code{proof-comment-start}}.
You should set this variable for reliable working of Proof General,