diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index f7eee781..7938e948 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1989,6 +1989,10 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." "Prompt for a command in the minibuffer and send it to proof assistant. The command isn't added to the locked region. +If a prefix arg is given and there is a selected region, that is +pasted into the command. This is handy for copying terms, etc from +the script. + If `proof-strict-state-preserving' is set, and `proof-state-preserving-p' is configured, then the latter is used as a check that the command will be safe to execute, in other words, that it won't ruin |