From db59e25fde60253848f2bfc8f22cf40c71ef46cd Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Fri, 6 Dec 2024 11:23:47 +0100 Subject: [PATCH] Drop lean4-default-*-name variables --- lean4-settings.el | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/lean4-settings.el b/lean4-settings.el index c1967f1..049c696 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -34,14 +34,6 @@ :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") :prefix "lean4-") -(defconst lean4-default-executable-name - (if (eq system-type 'windows-nt) "lean.exe" "lean") - "Default executable name of Lean.") - -(defconst lean4-default-lake-name - (if (eq system-type 'windows-nt) "lake.exe" "lake") - "Default executable name of Lake.") - (defcustom lean4-mode-hook (list #'lsp) "Hook run after entering `lean4-mode'." :options '(flycheck-mode lsp) @@ -53,12 +45,14 @@ :group 'lean4 :type 'string) -(defcustom lean4-executable-name lean4-default-executable-name +(defcustom lean4-executable-name + (if (eq system-type 'windows-nt) "lean.exe" "lean") "Name of lean executable." :group 'lean4 :type 'string) -(defcustom lean4-lake-name lean4-default-lake-name +(defcustom lean4-lake-name + (if (eq system-type 'windows-nt) "lake.exe" "lake") "Name of lake executable." :group 'lake :type 'string)