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

fix(emacs): actually initialize lean-company

Browse source
This commit is contained in:
Sebastian Ullrich 2016-10-14 17:48:33 -04:00
parent 541e9010e1
commit 71e01d2f89
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/emacs/lean-mode.el
View file

@ -305,6 +305,9 @@ enabled and disabled respectively.")
(when lean-flycheck-use
(lean-flycheck-turn-on)
(setq-local flycheck-disabled-checkers '()))
;; company-mode
(when lean-company-use
(company-lean-hook))
;; Draw a vertical line for rule-column
(when (and lean-rule-column
lean-show-rule-column-method)