diff options
| -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, |