max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(lean4-mode/lean4-util): (lean4-setup-rootdir) returns the wrong path

Browse source
This commit is contained in:
Sebastian Ullrich 2018-09-07 10:35:48 -07:00
parent 1a4a69679d
commit 845c496a07
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lean4-mode/lean4-mode.el
View file

@ -121,7 +121,7 @@
(easy-menu-define lean4-mode-menu lean4-mode-map
"Menu for the Lean major mode"
`("Lean"
`("Lean 4"
["Execute lean" lean4-execute t]
;; ["Create a new project" (call-interactively 'lean4-project-create) (not (lean4-project-inside-p))]
"-----------------"
@ -193,7 +193,7 @@ enabled and disabled respectively.")
;; Automode List
;;;###autoload
(define-derived-mode lean4-mode prog-mode "Lean"
(define-derived-mode lean4-mode prog-mode "Lean 4"
"Major mode for Lean
\\{lean4-mode-map}
Invokes `lean4-mode-hook'.

2
lean4-mode/lean4-util.el
View file

@ -14,7 +14,7 @@
(let ((root (executable-find lean4-executable-name)))
(when root
(setq lean4-rootdir (f-dirname (f-dirname root))))
root))
lean4-rootdir))
(defun lean4-get-rootdir ()
(if lean4-rootdir