fix(util/lean_path): relative position of library files in binary
distribution packages
This commit is contained in:
parent
c9132648a2
commit
3813aeede5
1 changed files with 4 additions and 1 deletions
|
@ -134,7 +134,10 @@ void init_lean_path(bool use_hott) {
|
|||
else
|
||||
*g_lean_path = exe_path + g_sep + ".." + g_sep + "library";
|
||||
*g_lean_path += g_path_sep;
|
||||
*g_lean_path += exe_path + g_sep + ".." + g_sep + "lib" + g_sep + "lean";
|
||||
if (use_hott)
|
||||
*g_lean_path += exe_path + g_sep + ".." + g_sep + "lib" + g_sep + "lean" + g_sep + "hott";
|
||||
else
|
||||
*g_lean_path += exe_path + g_sep + ".." + g_sep + "lib" + g_sep + "lean" + g_sep + "library";
|
||||
*g_lean_path += g_path_sep;
|
||||
*g_lean_path += ".";
|
||||
} else {
|
||||
|
|
Loading…
Reference in a new issue