merge from dev

This commit is contained in:
Daan Leijen 2024-12-17 00:14:03 -08:00
commit 63d0c8f861
14 changed files with 625 additions and 97 deletions

View file

@ -359,6 +359,7 @@ int main(int argc, char** argv) {
#else
mi_stats_print(NULL); // so we see rss/commit/elapsed
#endif
//mi_stats_print(NULL);
//bench_end_program();
return 0;
}