diff options
author | 1998-12-16 18:23:29 +0000 | |
---|---|---|
committer | 1998-12-16 18:23:29 +0000 | |
commit | a89ec35e4d846480a5e2c35748bb9fb7577aa5bb (patch) | |
tree | 87f9344be6279cd20f1bec098c73a5c8a588df05 /doc | |
parent | 65814b4f19e1e938afe7b2143dfdba1751599489 (diff) |
Updated magic.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/ProofGeneral.texi | 2 |
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 |