aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-17 14:23:15 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-01-17 14:23:15 +0000
commit8ec633ac5511ab74e5e37bf12727b4fee9678e85 (patch)
treed2857957e91823825d6fae74449a455b9d7a73a0 /doc
parentd470db2742f70a741df07a78568253a05ef1305a (diff)
Disable removal from input history
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi4
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