diff options
| author | Sébastien Hinderer <Sebastien.Hinderer@inria.fr> | 2022-01-08 16:07:53 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-01-10 17:12:06 +0100 |
| commit | 9d18d5a0b843dbea3c01ae52181674976ce6c2d6 (patch) | |
| tree | 5ccaef9450dab3573584c3d76b9a67f335008324 /tools | |
| parent | 001997e81342fd0d321fd877b73608150601e7d9 (diff) | |
| download | ocaml-9d18d5a0b843dbea3c01ae52181674976ce6c2d6.tar.gz | |
Remove mention of naked pointers from Inria CI scripts
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/inria/main | 3 | ||||
| -rwxr-xr-x | tools/ci/inria/other-configs/script | 3 |
2 files changed, 2 insertions, 4 deletions
diff --git a/tools/ci/inria/main b/tools/ci/inria/main index 630465924f..531d902ff3 100755 --- a/tools/ci/inria/main +++ b/tools/ci/inria/main @@ -237,8 +237,7 @@ export LC_ALL=C git clean -q -f -d -x if $flambda; then - confoptions="$confoptions --enable-flambda --enable-flambda-invariants \ ---disable-naked-pointers" + confoptions="$confoptions --enable-flambda --enable-flambda-invariants" fi eval ./configure "$CCOMP" $build $host --prefix='$instdir' $confoptions diff --git a/tools/ci/inria/other-configs/script b/tools/ci/inria/other-configs/script index 7ce82f40be..472098670d 100755 --- a/tools/ci/inria/other-configs/script +++ b/tools/ci/inria/other-configs/script @@ -38,9 +38,8 @@ ${main} -conf --disable-native-compiler \ -conf --disable-ocamldoc \ -conf --disable-dependency-generation \ -no-native -${main} -conf --disable-naked-pointers ${main} -with-bootstrap -conf --disable-flat-float-array -${main} -conf --enable-flambda -conf --disable-naked-pointers +${main} -conf --enable-flambda ${main} -conf --enable-reserved-header-bits=27 OCAMLRUNPARAM="c=1" ${main} ${main} -conf --with-pic |