Build with WITH_DBG_RUNTIME=false in ./bin/travis-ci

The debug runtimes are unused on TravisCI; this avoids unnecessary build time.
MatthewFluet · Jan 17, 2020 · 84d4861 · 84d4861
1 parent 18c6f0c
commit 84d4861
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/bin/travis-ci b/bin/travis-ci
@@ -19,7 +19,7 @@ fi
 MLTON_RUNTIME_ARGS="ram-slop 0.90"
 
 echo "Building MLton..."
-make CC="$CC" OLD_MLTON_RUNTIME_ARGS="$MLTON_RUNTIME_ARGS" MLTON_RUNTIME_ARGS="$MLTON_RUNTIME_ARGS" MLTON_COMPILE_ARGS="$MLTON_COMPILE_ARGS" all
+make CC="$CC" OLD_MLTON_RUNTIME_ARGS="$MLTON_RUNTIME_ARGS" MLTON_RUNTIME_ARGS="$MLTON_RUNTIME_ARGS" MLTON_COMPILE_ARGS="$MLTON_COMPILE_ARGS" WITH_DBG_RUNTIME=false all
 
 if [ "$REGRESSION" == "true" ]; then
 echo "Running regression tests..."