merge from dev

This commit is contained in:
Daan Leijen 2022-04-20 17:16:25 -07:00
commit f2a2eb4ad0
23 changed files with 1625 additions and 317 deletions

View file

@ -257,7 +257,7 @@ int main(int argc, char** argv) {
mi_collect(true);
#endif
mi_stats_print(NULL);
#endif
#endif
//bench_end_program();
return 0;
}