max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(emacs/lean-server): put face into lean group for customization

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-18 14:36:12 +01:00 • committed by Leonardo de Moura
parent be6b81db07
commit bf20be51d5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/emacs/lean-server.el
View file

@ -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))