From 8ec633ac5511ab74e5e37bf12727b4fee9678e85 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 17 Jan 2008 14:23:15 +0000 Subject: Disable removal from input history --- doc/ProofGeneral.texi | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'doc') 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 -- cgit v1.2.3