From a9712b91a82415ccad41de5237b99092e17be056 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Dec 2013 16:18:27 -0800 Subject: [PATCH] feat(util/lean_path): include ../library in the default LEAN_PATH Signed-off-by: Leonardo de Moura --- src/util/lean_path.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index 9ae78c3fe..7010f674f 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -91,8 +91,11 @@ struct init_lean_path { char * r = getenv("LEAN_PATH"); if (r == nullptr) { g_lean_path = "."; + std::string exe_path = get_path(get_exe_location()); g_lean_path += g_path_sep; - g_lean_path += get_path(get_exe_location()); + g_lean_path += exe_path + g_sep + ".." + g_sep + "library"; + g_lean_path += g_path_sep; + g_lean_path += exe_path; } else { g_lean_path = r; }