merge in dev branch

2019-07-02 17:28:15 -07:00
parent 8cb36c62e6 5c0ffe9865
commit cec3c4f9ff
3 changed files with 3 additions and 5 deletions
--- a/src/os.c
+++ b/src/os.c
@@ -415,6 +415,7 @@ bool _mi_os_decommit(void* addr, size_t size, mi_stats_t* stats) {
  return mi_os_commitx(addr, size, false, stats);
 }

+
 /* -----------------------------------------------------------
  OS allocation using mmap/munmap
 ----------------------------------------------------------- */