aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorLawrence Dunn2020-04-02 12:56:27 -0400
committerLawrence Dunn2020-04-02 12:56:27 -0400
commita03dc31801972cbcff38035a30711da34d66ed78 (patch)
treecc055dd0397f55e845308485c3c2586b4b59a9a7
parent71748af5bc0f813d4c6a42f303d2c2cec85b3c9a (diff)
Correct documentation
-rw-r--r--doc/ProofGeneral.texi3
1 files changed, 1 insertions, 2 deletions
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.