aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-01-12 14:47:42 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-01-12 14:47:42 +0000
commitc91f610f662a1357522a12276ee51e8cb18fce91 (patch)
tree4a35112904dd3ae38ab9ceae55d16643083bd687 /doc
parent8d537dbdc8bc44f1b2cb66442b5bef6523dc484a (diff)
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi12
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 8138c1af..a8cf718d 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1858,13 +1858,13 @@ to a slower interactive loop with display updates.
In the check next command mode, the successfully checked region will
briefly flash up as green to indicate it is okay.
-You can use @kbd{C-c C-.} (@code{proof-goto-end-of-locked}) to find
-out where processing got to, as usual. Text is only sent if the last
+You can use @kbd{C-c C-.} (@code{proof-goto-end-of-locked}) to find out
+where processing got to, as usual. Text is only sent if the last
interactive command processed some text (i.e., wasn't an undo step
-backwards into the buffer) and processing didn't stop with an error.
-To start automatic processing again after an error, simply hit
-@kbd{C-c C-n}. To turn the automatic processing on or off from the
-keyboard, you can use the keybinding:
+backwards into the buffer) and processing didn't stop with an error. To
+start automatic processing again after an error, simply hit @kbd{C-c
+C-n} after editing the buffer. To turn the automatic processing on or
+off from the keyboard, you can use the keybinding:
@table @kbd
@item C-c >