merge from dev with the destroy_on_exit option

This commit is contained in:
Daan Leijen 2022-11-21 10:03:52 -08:00
commit 163afcce75
8 changed files with 68 additions and 8 deletions

View file

@ -342,6 +342,7 @@ typedef enum mi_option_e {
mi_option_allow_decommit,
mi_option_segment_decommit_delay,
mi_option_decommit_extend_delay,
mi_option_destroy_on_exit,
_mi_option_last
} mi_option_t;