diff options
| -rw-r--r-- | plastic/plastic.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plastic/plastic.el b/plastic/plastic.el index 5c6c05bd..6eb8061c 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -638,7 +638,7 @@ We assume that module identifiers coincide with file names." (defun plastic-send-one-undo () "send an Undo cmd" - (proof-send (concat plastic-lit-string " &S Undo;"))) + (proof-shell-insert (concat plastic-lit-string " &S Undo;"))) (defun plastic-try-cmd () "undo whatever was tried, if error-free" |