From dc0e6861b7ed912d78ebdb93282cfc25a3f2160e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Oct 2014 02:27:52 -0700 Subject: [PATCH] fix(emacs/lean-mode): wrong pp highlighting, fixes #225 --- src/emacs/lean-mode.el | 1 + 1 file changed, 1 insertion(+) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 9ce72d8270..f71056a547 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -200,6 +200,7 @@ Invokes `lean-mode-hook'. (set (make-local-variable 'comment-use-syntax) t) (set (make-local-variable 'font-lock-defaults) lean-font-lock-defaults) (set (make-local-variable 'indent-tabs-mode) nil) + (set 'compilation-mode-font-lock-keywords '()) (set-input-method "Lean") (set (make-local-variable 'lisp-indent-function) 'common-lisp-indent-function)