From f98ab2a8ff961ed6c8085f83816506243105d4ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Aug 2014 11:16:29 -0700 Subject: [PATCH] fix(src/emacs/lean-syntax.el): remove obsolete command set_opaque Signed-off-by: Leonardo de Moura --- src/emacs/lean-syntax.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 2057c63a3..651ae94b7 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -72,7 +72,7 @@ (zero-or-more (or whitespace "{" "[")) (group (zero-or-more (not whitespace)))) (2 'font-lock-function-name-face)) - ("\\(set_opaque\\|set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face)) + ("\\(set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face)) ;; place holder (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) ;; sorry