Inria CI main job fix
This commit stops enabling the instrumented and debug runtime at configure time. Given that they are now enabled by default this is no longer necessary.master
parent
6f1c0708a7
commit
a9186772fe
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue