diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index b554cd33..7ba83acc 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2120,7 +2120,9 @@ edit of it. The feature is reminiscent of history mechanisms provided in shell terminals (and the implementation is borrowed from the Emacs Comint package). The input ring only contains commands which have been successfully processed (coloured blue). Duplicated commands are only -entered once. When commands are undone, they are removed from the ring. +entered once. +@c this is disabled for now, it's not robust +@c When commands are undone, they are removed from the ring. The size of the ring is set by the variable @code{pg-input-ring-size}. @kindex M-p |