diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index b30e8643..8138c1af 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2455,6 +2455,8 @@ Fraktur font face. @deffn Face unicode-tokens-script-font-face Script font face. @end deffn + + @node Moving between Unicode and tokens @section Moving between Unicode and tokens |