From dea1e52c96e702f559129b852409ee94b7ca6995 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Jul 2019 16:15:38 -0700
Subject: [PATCH] feat(shell/lean): initialize searchPath implemented in Lean

---
 src/shell/lean.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index c75b9ee4fb..0273ae5c85 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -296,6 +296,12 @@ object* test_module_parser_core(object* env, object* input, object* filename, ui
 bool test_module_parser(environment const & env, std::string const & input, std::string const & filename) {
     return get_io_scalar_result<bool>(test_module_parser_core(env.to_obj_arg(), mk_string(input), mk_string(filename), false, io_mk_world()));
 }
+
+object* init_search_path_core(object* opt_path, object* w);
+
+void init_search_path() {
+    get_io_scalar_result<unsigned>(init_search_path_core(mk_option_none(), io_mk_world()));
+}
 }
 
 int main(int argc, char ** argv) {
@@ -335,6 +341,8 @@ int main(int argc, char ** argv) {
     bool json_output = false;
 #endif
 
+    init_search_path();
+
     search_path path = get_lean_path_from_env().value_or(get_builtin_search_path());
 
     options opts;