From bf20be51d571fa5cdc3e568aced0b529fa3037ea Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 18 Jan 2017 14:36:12 +0100 Subject: [PATCH] chore(emacs/lean-server): put face into lean group for customization --- src/emacs/lean-server.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el index 33d9ce558f..4cd549f8de 100644 --- a/src/emacs/lean-server.el +++ b/src/emacs/lean-server.el @@ -206,8 +206,8 @@ (((class color) (background dark)) :background "salmon4") (t :inverse-video t)) - "Face to highlight running Lean tasks." - :group 'lean-server-faces) + "Face to highlight pending Lean tasks." + :group 'lean) (defun lean-server-update-task-overlays (&optional buf) (dolist (ov lean-server-task-overlays) (delete-overlay ov))