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

fix: leak in lean_mk_array

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-07 18:20:32 +02:00
parent 05b12e2b61
commit 7b128b308b
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/runtime/object.cpp
View file

@ -2026,7 +2026,11 @@ extern "C" object * lean_mk_array(obj_arg n, obj_arg v) {
for (; it != end; ++it) {
*it = v;
}
if (sz > 1) lean_inc_n(v, sz - 1);
if (sz == 0) {
lean_dec(v);
} else if (sz > 1) {
lean_inc_n(v, sz - 1);
}
return r;
}