michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(emacs/lean-mode): enable company-etags in lean-mode

Browse source
This commit is contained in:
Soonho Kong 2014-08-21 09:34:29 -07:00
parent 272c463182
commit 39f9826dca
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -109,8 +109,9 @@
(eldoc-mode +1)
(when lean-company-use
(require 'company)
(set (make-local-variable 'company-backends) '(company-etags))
(company-mode t))))
(company-mode t)
(add-to-list 'company-etags-modes 'lean-mode)
(set (make-local-variable 'company-backends) '(company-etags)))))
"A mode for Lean files" ;; doc string for this mode
)