diff --git a/tools/ci/inria/other-configs b/tools/ci/inria/other-configs index accd724f8..7ec331d75 100755 --- a/tools/ci/inria/other-configs +++ b/tools/ci/inria/other-configs @@ -24,6 +24,6 @@ main="${mainjob} -j8" ${main} -conf --disable-native-compiler -no-native ${main} -conf --disable-naked-pointers -${main} -conf --disable-flat-float-array +${main} -with-bootstrap -conf --disable-flat-float-array ${main} -conf --enable-flambda -conf --disable-naked-pointers OCAMLRUNPARAM="c=1" ${main}