diff --git a/bin/travis-ci b/bin/travis-ci index 84cd78c6d..f4db765c1 100755 --- 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..."