diff options
Diffstat (limited to 'tools/ci/inria/main')
| -rwxr-xr-x | tools/ci/inria/main | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/ci/inria/main b/tools/ci/inria/main index ebed3e694b..30db36e9ae 100755 --- a/tools/ci/inria/main +++ b/tools/ci/inria/main @@ -226,7 +226,8 @@ export LC_ALL=C git clean -q -f -d -x if $flambda; then - confoptions="$confoptions --enable-flambda --enable-flambda-invariants" + confoptions="$confoptions --enable-flambda --enable-flambda-invariants \ +--disable-naked-pointers" fi eval ./configure "$CCOMP" $build $host --prefix='$instdir' $confoptions |