michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(util/lean_path.cpp): use '/library' as LEAN_PATH for emscripten

Browse source
This commit is contained in:
Soonho Kong 2014-10-14 18:56:52 -07:00
parent c92260d9ec
commit e99463980a
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/util/lean_path.cpp
View file

@ -119,6 +119,10 @@ static std::string * g_lean_path = nullptr;
static std::vector<std::string> * g_lean_path_vector = nullptr;
void init_lean_path() {
#if defined(LEAN_EMSCRIPTEN)
*g_lean_path = "/library";
g_lean_path_vector->push_back(*g_lean_path);
#else
char * r = getenv("LEAN_PATH");
if (r == nullptr) {
*g_lean_path = ".";
@ -144,6 +148,7 @@ void init_lean_path() {
}
if (j > i)
g_lean_path_vector->push_back(g_lean_path->substr(i, j - i));
#endif
}
static char g_sep_str[2];