diff --git a/tools/ci/inria/main b/tools/ci/inria/main index 11e41fee3..f164557bc 100755 --- a/tools/ci/inria/main +++ b/tools/ci/inria/main @@ -117,7 +117,6 @@ case "${OCAML_ARCH}" in bsd) make=gmake ;; macos) ;; linux) - confoptions="${confoptions} -with-instrumented-runtime" check_make_alldepend=true ;; cygwin) @@ -199,7 +198,6 @@ git clean -f -d -x case $configure in unix) - confoptions="$confoptions -with-debug-runtime" if $flambda; then confoptions="$confoptions -flambda -with-flambda-invariants" fi