merge from dev

This commit is contained in:
Daan Leijen 2020-12-10 13:17:56 -08:00
commit b803095b83
8 changed files with 42 additions and 17 deletions

View file

@ -319,6 +319,7 @@ typedef enum mi_option_e {
mi_option_limit_os_alloc,
mi_option_os_tag,
mi_option_max_errors,
mi_option_max_warnings,
_mi_option_last
} mi_option_t;