aboutsummaryrefslogtreecommitdiffhomepage
path: root/plastic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-15 14:58:24 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-15 14:58:24 +0000
commit63ea80bc2435798a59822790bb09b5d19bc27777 (patch)
tree044c4f24e3f6abc8f9ecea765d8fa5fb9c1ea4c3 /plastic
parent451afba1f6ed2adf81a27d1afa8bd5ec578a0d1e (diff)
Removed proof-try-command.
Diffstat (limited to 'plastic')
-rw-r--r--plastic/plastic.el3
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 ()