aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-07 09:22:28 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-07 09:22:28 +0000
commitb581ed2eec722cc763f5c2fa5c8bb536532a4796 (patch)
treec237229da1c44857220793768e62e8cae9b411d7 /lego
parentff4011ea21dee63ffe62be170c16a58f7b011b87 (diff)
lego-shell-process-output -> lego-shell-classify-output
Diffstat (limited to 'lego')
-rw-r--r--lego/lego.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/lego/lego.el b/lego/lego.el
index 9dc7dd47..73552f20 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -44,7 +44,7 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Users should not need to change this.
-(defvar lego-shell-process-output
+(defvar lego-shell-classify-output
'((lambda (cmd string) (proof-string-match "^Module" cmd)) .
(lambda (cmd string)
(setq proof-shell-delayed-output
@@ -402,7 +402,7 @@ For LEGO, we assume that module identifiers coincide with file names."
proof-shell-init-cmd lego-process-config
proof-shell-restart-cmd lego-process-config
pg-subterm-anns-use-stack nil
- proof-shell-process-output-system-specific lego-shell-process-output
+ proof-shell-classify-output-system-specific lego-shell-classify-output
lego-shell-current-line-width nil
;; LEGO uses Unicode escape prefix: liable to create problems