From c9ffc2fec8614e80513c151b66888418e83c718f Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Fri, 27 Feb 2015 15:27:18 -0500
Subject: [PATCH] fix(emacs/lean-util): add hlean support in lean-path-list

close #450
---
 src/emacs/lean-util.el | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/emacs/lean-util.el b/src/emacs/lean-util.el
index 7a0c90f34..4db8b1fdb 100644
--- a/src/emacs/lean-util.el
+++ b/src/emacs/lean-util.el
@@ -51,10 +51,15 @@
   (interactive)
   (let* ((lean-path-env-list
           (parse-colon-path (getenv "LEAN_PATH")))
+         (lean-mode-option
+          (pcase (lean-choose-minor-mode-based-on-extension)
+            (`standard "--lean")
+            (`hott     "--hlean")))
          (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))))