diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2007-05-10 23:21:38 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2007-05-10 23:21:38 +0000 |
commit | 8cce4ea2efb759bec1909576fd42ed34b8c0a385 (patch) | |
tree | b757364600e7cb2e73536d7f5a880b75558baca7 /lego | |
parent | 55455661fc98b43692b4b3a51aa5ea3b25a3846e (diff) |
Disable unicode use on LEGO, uses escape prefix
Diffstat (limited to 'lego')
-rw-r--r-- | lego/lego.el | 3 |
1 files changed, 3 insertions, 0 deletions
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))) |