From 8cce4ea2efb759bec1909576fd42ed34b8c0a385 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 10 May 2007 23:21:38 +0000 Subject: Disable unicode use on LEGO, uses escape prefix --- lego/lego.el | 3 +++ 1 file changed, 3 insertions(+) (limited to 'lego') diff --git a/lego/lego.el b/lego/lego.el index e2f755ea..7a15ab29 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -419,6 +419,9 @@ We assume that module identifiers coincide with file names." proof-shell-process-output-system-specific lego-shell-process-output lego-shell-current-line-width nil + ;; LEGO uses Unicode escape prefix: liable to create problems + proof-shell-unicode nil + proof-shell-process-file (cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]" (lambda (str) (let ((match (match-string 2 str))) -- cgit v1.2.3