From 01666572d7c342cde52a7a95087c322a3505057d Mon Sep 17 00:00:00 2001 From: Henrik Lissner Date: Sun, 12 Jan 2025 20:13:49 -0500 Subject: [PATCH] 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@11196af3122f Fix: #8159 --- modules/lang/lean/README.org | 1 - modules/lang/lean/config.el | 8 -------- modules/lang/lean/packages.el | 3 --- 3 files changed, 12 deletions(-) diff --git a/modules/lang/lean/README.org b/modules/lang/lean/README.org index cf2f92fff..e12c17632 100644 --- a/modules/lang/lean/README.org +++ b/modules/lang/lean/README.org @@ -14,7 +14,6 @@ This module adds support for the [[https://leanprover.github.io/about/][Lean pro ** Packages - [[doom-package:lean-mode]] -- [[doom-package:company-lean]] if [[doom-module::completion company]] ** TODO Hacks #+begin_quote diff --git a/modules/lang/lean/config.el b/modules/lang/lean/config.el index d706630f3..70c984e2e 100644 --- a/modules/lang/lean/config.el +++ b/modules/lang/lean/config.el @@ -26,11 +26,3 @@ "h" #'lean-hole "m" #'lean-message-boxes-toggle "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)) diff --git a/modules/lang/lean/packages.el b/modules/lang/lean/packages.el index 7a3640530..d4d415a96 100644 --- a/modules/lang/lean/packages.el +++ b/modules/lang/lean/packages.el @@ -2,6 +2,3 @@ ;;; lang/lean/packages.el (package! lean-mode :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a") - -(when (modulep! :completion company) - (package! company-lean :pin "99d6a34dc5b12f6e996e9217fa9f6fe4a6af037a"))