diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2000-10-02 17:47:33 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2000-10-02 17:47:33 +0000 |
commit | 781e80c6a69cac7b991207fae312a305d8ff6a55 (patch) | |
tree | fb945570ec5ed8543515054d619dc94914a7a2b8 | |
parent | ffc8dbe7f626581b60a32c53a6ccc5b14b88279f (diff) |
Updated magic
-rw-r--r-- | doc/PG-adapting.texi | 2 |
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, |