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

fix(util/lean_path): memory leak

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-06 10:22:45 -08:00
parent c33928f202
commit 5f182dc1cc
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/util/lean_path.cpp
View file

@ -29,7 +29,9 @@ file_not_found_exception::file_not_found_exception(std::string const & fname):
exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH"),
m_fname(fname) {}
static std::string * g_default_file_name = nullptr;
static std::string * g_default_file_name = nullptr;
static std::string * g_lean_path = nullptr;
static std::vector<std::string> * g_lean_path_vector = nullptr;
bool is_directory(char const * pathname) {
struct stat info;
@ -115,9 +117,6 @@ std::string get_path(std::string f) {
}
}
static std::string * g_lean_path = nullptr;
static std::vector<std::string> * g_lean_path_vector = nullptr;
void init_lean_path(bool use_hott) {
#if defined(LEAN_EMSCRIPTEN)
*g_lean_path = "/library";
@ -161,6 +160,8 @@ void init_lean_path(bool use_hott) {
static char g_sep_str[2];
void initialize_lean_path(bool use_hott) {
if (g_default_file_name != nullptr)
finalize_lean_path();
g_default_file_name = new std::string(LEAN_DEFAULT_MODULE_FILE_NAME);
g_lean_path = new std::string();
g_lean_path_vector = new std::vector<std::string>();