diff options
Diffstat (limited to 'plastic/plastic.el')
| -rw-r--r-- | plastic/plastic.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plastic/plastic.el b/plastic/plastic.el index a8a1e6b1..0678042f 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -653,7 +653,8 @@ We assume that module identifiers coincide with file names." "undo whatever was tried, if error-free" (interactive) (plastic-reset-error) - (proof-try-command) + (let ((proof-state-preserving-p nil)) ; allow any command + (proof-execute-minibuffer-cmd)) (plastic-call-if-no-error 'plastic-send-one-undo)) (defun plastic-minibuf () |