From 6fa246032fe0ef6d8301a0cdd6c6e7973bf33bed Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sat, 31 Dec 2016 15:15:20 +0100 Subject: [PATCH] fix(library/native_compiler): get_exe_location does not exist on emscripten --- src/library/native_compiler/native_compiler.cpp | 4 ++++ src/util/lean_path.h | 2 ++ 2 files changed, 6 insertions(+) diff --git a/src/library/native_compiler/native_compiler.cpp b/src/library/native_compiler/native_compiler.cpp index ee2a75403f..073bfc0041 100644 --- a/src/library/native_compiler/native_compiler.cpp +++ b/src/library/native_compiler/native_compiler.cpp @@ -51,8 +51,12 @@ expr mk_local(name const & n) { void initialize_install_path() { // 8 is the size of the string bin/lean which we want to remove from // the installed version of Lean. +#if defined(LEAN_EMSCRIPTEN) + g_lean_install_path = new std::string; +#else auto path = get_exe_location(); g_lean_install_path = new std::string(path.substr(0, path.size() - 8)); +#endif } std::string get_install_path() { diff --git a/src/util/lean_path.h b/src/util/lean_path.h index 0881d20e03..4683cbabfb 100644 --- a/src/util/lean_path.h +++ b/src/util/lean_path.h @@ -20,7 +20,9 @@ public: /** \brief Initialize the lean_path */ void init_lean_path(); +#if !defined(LEAN_EMSCRIPTEN) std::string get_exe_location(); +#endif /** \brief Return the LEAN_PATH string */ char const * get_lean_path();