diff options
| -rw-r--r-- | doc/PG-adapting.texi | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 18f36906..14c3bda2 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2443,7 +2443,6 @@ in addition to the four modes for Proof General (script, shell, response, pbp). Set this variable if you want additional modes to also display tokens (for example, editing documentation or source code files). @end defvar -@end defvar |