diff options
| -rw-r--r-- | doc/PG-adapting.texi | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 7dbef061..39cbecf6 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2405,13 +2405,10 @@ This hook is called before fonfitying a region in an output buffer.@* @node Configuring Tokens @chapter Configuring Tokens -@cindex X-Symbol @cindex Unicode Tokens @cindex Tokens -The Tokens package is described in the Proof General user manual. To -configure Tokens for Proof General, you must understand a little bit -of how X-Symbol works: read the documentation that is supplied with it. +The Tokens package is described in the Proof General user manual. @c TEXI DOCSTRING MAGIC: proof-tokens-activate-command @defvar proof-tokens-activate-command |