aboutsummaryrefslogtreecommitdiff
path: root/plastic
diff options
context:
space:
mode:
authorDavid Aspinall1999-11-22 18:52:47 +0000
committerDavid Aspinall1999-11-22 18:52:47 +0000
commite4ce3196f9e265b43dc85e2b21097890ad7b152a (patch)
tree340b5345b03e054cb0b45c6fc2afd32a63d77cf5 /plastic
parent943b92c15f616944b6b48e35fecf0fb31ce40c0e (diff)
proof-shell-done-invisible -> proof-done-invisible again
Diffstat (limited to 'plastic')
-rw-r--r--plastic/plastic.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 30561b16..f9ee3df8 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -654,7 +654,7 @@ We assume that module identifiers coincide with file names."
;; Interface to proof-shell-insert now requires two args (for the
;; sake of plastic!) and shouldn't be called from PG instances
(proof-shell-insert (concat plastic-lit-string " &S Undo;")
- 'proof-shell-done-invisible))
+ 'proof-done-invisible))
(defun plastic-try-cmd ()
"undo whatever was tried, if error-free"