diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index e0f22c5865..efcfa71284 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -126,7 +126,7 @@ (defun lean-exec-at-pos (process-name process-buffer-name &rest options) "Execute Lean by providing current position with optional -agruments. The output goes to 'process-buffer-name' buffer, which +arguments. The output goes to 'process-buffer-name' buffer, which will be flushed everytime it's executed." (setq g-lean-exec-at-pos-buf "") ;; Kill process-name if exists @@ -152,12 +152,10 @@ will be flushed everytime it's executed." (if (s-equals? (buffer-file-name) target-file-name) `("--cache" ,cache-file-name) '())) - (lean-mode-option "--lean") (default-directory (or (lean-project-find-root) default-directory)) (process-args (append `(,process-name ,process-buffer-name ,(lean-get-executable lean-executable-name) - ,lean-mode-option "--dir" ,(f-dirname (buffer-file-name)) "--line" diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el index 8a400871b5..f61b499c0e 100644 --- a/src/emacs/lean-util.el +++ b/src/emacs/lean-util.el @@ -46,12 +46,10 @@ (interactive) (let* ((lean-path-env-list (parse-colon-path (getenv "LEAN_PATH"))) - (lean-mode-option "--lean") (lean--path-list (parse-colon-path (ignore-errors (car (process-lines (lean-get-executable lean-executable-name) - lean-mode-option "--path"))))) (project-dir (f--traverse-upwards (f-exists? (f-expand ".project" it)) (f-dirname (buffer-file-name))))