merge from dev

This commit is contained in:
daan 2019-08-20 07:37:46 -07:00
commit 7a2e0df5ea
7 changed files with 37 additions and 37 deletions

View file

@ -425,7 +425,7 @@ static void mi_process_load(void) {
if (mi_option_is_enabled(mi_option_reserve_huge_os_pages)) {
size_t pages = mi_option_get(mi_option_reserve_huge_os_pages);
double max_secs = (double)pages / 10.0; // 0.1s per page
double max_secs = (double)pages / 5.0; // 0.2s per page
mi_reserve_huge_os_pages(pages, max_secs);
}
}