From 9d18d5a0b843dbea3c01ae52181674976ce6c2d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Hinderer?= <Sebastien.Hinderer@inria.fr>
Date: Sat, 8 Jan 2022 16:07:53 +0100
Subject: Remove mention of naked pointers from Inria CI scripts

---
 tools/ci/inria/main                 | 3 +--
 tools/ci/inria/other-configs/script | 3 +--
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'tools')

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
-- 
cgit v1.2.1