aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-12-16 18:23:29 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-12-16 18:23:29 +0000
commita89ec35e4d846480a5e2c35748bb9fb7577aa5bb (patch)
tree87f9344be6279cd20f1bec098c73a5c8a588df05 /doc
parent65814b4f19e1e938afe7b2143dfdba1751599489 (diff)
Updated magic.
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 8b83116b..c246221a 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1066,7 +1066,7 @@ the text is also deleted from the proof script.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-retract-until-point-interactive
-@deffn Command proof-retract-until-point-interactive delete-region
+@deffn Command proof-retract-until-point-interactive &optional delete-region
Tell the proof process to retract until point.
If invoked outside a locked region, undo the last successfully processed
command. If called with a prefix argument (@var{delete-region} non-nil), also