aboutsummaryrefslogtreecommitdiffhomepage
path: root/plastic
diff options
context:
space:
mode:
authorGravatar Paul Callaghan <p.c.callaghan@durham.ac.uk>1999-05-12 14:16:47 +0000
committerGravatar Paul Callaghan <p.c.callaghan@durham.ac.uk>1999-05-12 14:16:47 +0000
commit35415802db09738fabb5d3fc04eaf11c0f26249a (patch)
tree9c82ee5fd2f9134d01f02e686dce26d220614505 /plastic
parent12bab96eea4c44ebe27eecfb31f49ced67008dac (diff)
changed use of proof-send (OLD) to proof-shell-insert
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 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"