mirror of
https://github.com/doomemacs/doomemacs.git
synced 2025-12-06 02:30:33 -08:00
fix(lean): remove company-lean
company-lean was removed from MELPA. Since lean4 support is around the corner and Doom has deprecated its support for Company, I'll simply remove this package. Ref: melpa/melpa@11196af312 Fix: #8159
This commit is contained in:
parent
40b9ad7b7c
commit
01666572d7
3 changed files with 0 additions and 12 deletions
|
|
@ -14,7 +14,6 @@ This module adds support for the [[https://leanprover.github.io/about/][Lean pro
|
||||||
|
|
||||||
** Packages
|
** Packages
|
||||||
- [[doom-package:lean-mode]]
|
- [[doom-package:lean-mode]]
|
||||||
- [[doom-package:company-lean]] if [[doom-module::completion company]]
|
|
||||||
|
|
||||||
** TODO Hacks
|
** TODO Hacks
|
||||||
#+begin_quote
|
#+begin_quote
|
||||||
|
|
|
||||||
|
|
@ -26,11 +26,3 @@
|
||||||
"h" #'lean-hole
|
"h" #'lean-hole
|
||||||
"m" #'lean-message-boxes-toggle
|
"m" #'lean-message-boxes-toggle
|
||||||
"e" #'lean-execute))
|
"e" #'lean-execute))
|
||||||
|
|
||||||
|
|
||||||
(use-package! company-lean
|
|
||||||
:when (modulep! :completion company)
|
|
||||||
:after lean-mode
|
|
||||||
:init
|
|
||||||
(advice-add #'company-lean-hook :override #'ignore)
|
|
||||||
(set-company-backend! 'lean-mode 'company-lean))
|
|
||||||
|
|
|
||||||
|
|
@ -2,6 +2,3 @@
|
||||||
;;; lang/lean/packages.el
|
;;; lang/lean/packages.el
|
||||||
|
|
||||||
(package! lean-mode :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a")
|
(package! lean-mode :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a")
|
||||||
|
|
||||||
(when (modulep! :completion company)
|
|
||||||
(package! company-lean :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a"))
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue