Drop lean4-default-*-name variables

leanprover-community · Dec 10, 2024 · db59e25 · db59e25
1 parent 65948f3
commit db59e25
Showing 1 changed file with 4 additions and 10 deletions.
diff --git 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)