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':