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

fix(frontends/lean/inductive_cmds): memory leak

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-23 15:36:46 -07:00
parent 871d78fbf8
commit 6aa11be6fd
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/inductive_cmds.cpp
View file

@ -540,6 +540,7 @@ void initialize_inductive_cmds() {
g_tmp_prefix = new name(name::mk_internal_unique_name());
}
void finalize_inductive_cmds() {}
void finalize_inductive_cmds() {
delete g_tmp_prefix;
}
}