Merge branch 'dev' into dev-exp

2019-08-20 08:27:46 -07:00
parent 5b2f4184b3 27d794b5f4
commit 86d4ded831
13 changed files with 80 additions and 66 deletions
--- a/test/test-api.c
+++ b/test/test-api.c
@@ -66,7 +66,7 @@ bool test_heap2();
 // Main testing
 // ---------------------------------------------------------------------------
 int main() {
-  mi_option_enable(mi_option_verbose,false);
+  mi_option_disable(mi_option_verbose);

  // ---------------------------------------------------
  // Malloc