max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(checker): do not set LEAN_PATH unnecessarily

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-24 11:36:14 +01:00
parent 661dd9c8a3
commit 32c97df697
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/checker/checker.cpp
View file

@ -25,11 +25,6 @@ using namespace lean; // NOLINT
int main(int argc, char ** argv) {
#if defined(LEAN_EMSCRIPTEN)
EM_ASM(
var lean_path = process.env['LEAN_PATH'];
if (lean_path) {
ENV['LEAN_PATH'] = lean_path;
}
try {
// emscripten cannot mount all of / in the vfs,
// we can only mount subdirectories...