From a38887058166487607f03972d6d2c25ee9d5dada Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Wed, 1 Apr 2020 17:46:21 -0400
Subject: SearchAbout is deprecated since 8.5; use Search instead

---
 doc/ProofGeneral.texi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 23aba63b..699b304b 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4342,7 +4342,7 @@ The same for a ``Print '' query.
 @item C-c C-a C-b
 The same for a ``About '' query.
 @item C-c C-a C-a
-The same for a ``SearchAbout '' query (no C-u prefix).
+The same for a ``Search '' query (no C-u prefix).
 @item C-c C-a C-o
 The same for a Search ``SearchIsos'' (no C-u prefix).
 
-- 
cgit v1.2.3


From a03dc31801972cbcff38035a30711da34d66ed78 Mon Sep 17 00:00:00 2001
From: Lawrence Dunn
Date: Thu, 2 Apr 2020 12:56:27 -0400
Subject: Correct documentation

---
 doc/ProofGeneral.texi | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 699b304b..5f1e8231 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -924,8 +924,7 @@ example in Isabelle with semi-colons, but these will not appear in the
 final text.
 
 Coq, on the other hand, requires a full-stop terminator at the end of
-each line, so @kbd{C-c .} is the key binding used to turn on
-electric terminator.  If you don't know what the terminator character
+each line. If you don't know what the terminator character
 is, you can find the option anyway on the menu:
 @code{Proof-General -> Quick Options -> Processing -> Electric Terminator}
 which also shows the key binding.
-- 
cgit v1.2.3


From 1f56706ff2f0870a461ded0f5a40292df8bcd96a Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Thu, 2 Apr 2020 20:20:00 +0200
Subject: Rephrase ProofGeneral.texi following PR #476 that fixed #475

Note that currently, there is no keybinding associated to the electric
terminator.
---
 doc/ProofGeneral.texi | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 5f1e8231..c2cb3be5 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -924,17 +924,15 @@ example in Isabelle with semi-colons, but these will not appear in the
 final text.
 
 Coq, on the other hand, requires a full-stop terminator at the end of
-each line. If you don't know what the terminator character
-is, you can find the option anyway on the menu:
+each line. If you want to enable electric terminator, use the menu item:
 @code{Proof-General -> Quick Options -> Processing -> Electric Terminator}
-which also shows the key binding.
-
-If you want to use electric terminator, you can customize Proof
-General to enable it every time if you want, @xref{Customizing Proof
-General}.  For the common options, customization is easy: just
-use the menu item @code{Proof General -> Quick Options} to make your choices,
-and @code{Proof-General -> Quick Options -> Save Options} to
-save your choices.
+
+If you want to keep electric terminator enabled all the time, you can
+customize Proof General to do so, @xref{Customizing Proof General}.  For
+the common options, customization is easy: just use the menu item
+@code{Proof General -> Quick Options} to make your choices, and
+@code{Proof-General -> Quick Options -> Save Options} to save your
+choices.
 
 
 
-- 
cgit v1.2.3