aboutsummaryrefslogtreecommitdiff
path: root/generic/proof-script.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r--generic/proof-script.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index b7be033e..d9ef6d44 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,6 +1,6 @@
;;; proof-script.el --- Major mode for proof assistant script files.
;;
-;; Copyright (C) 1994-2008 LFCS Edinburgh.
+;; Copyright (C) 1994-2009 LFCS Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
@@ -2227,7 +2227,7 @@ appropriate."
;;;###autoload
(defun proof-insert-sendback-command (cmd)
"Insert CMD into the proof script, execute assert-until-point."
- (let (span)
+ (proof-with-script-buffer
(proof-goto-end-of-locked)
(insert "\n") ;; could be user opt
(insert cmd)