From d00c013ad825df6f58ae5a513dec5b0a40e88aa2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Feb 2015 15:08:13 -0800
Subject: [PATCH] fix(shell/lean): display HoTT library path for `lean --hlean
 --path`

See #450
---
 src/shell/lean.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index cb2f04a3f..aff055f03 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -382,6 +382,8 @@ int main(int argc, char ** argv) {
             script_state::set_check_interrupt_freq(atoi(optarg));
             break;
         case 'p':
+            if (default_k == input_kind::HLean)
+                lean::initialize_lean_path(true);
             std::cout << lean::get_lean_path() << "\n";
             return 0;
         case 's':