summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2020-06-14 11:23:35 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2020-06-22 14:20:05 +0200
commit41227a1ebaf9bc519d112682f1e1ae3bfb3960a8 (patch)
tree40871ff64a8962560b89e2ea4f65a67c3d8ec9eb /configure
parentb18ac65d897df9b6c9d268ca5a3f0ff61433beba (diff)
downloadocaml-41227a1ebaf9bc519d112682f1e1ae3bfb3960a8.tar.gz
configure: add a NAKED_POINTERS parameter to Makefile.config
We have NAKED_POINTERS=false if configured with --disable-naked-pointers, NAKED_POINTERS=true otherwise.
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure7
1 files changed, 6 insertions, 1 deletions
diff --git a/configure b/configure
index cb12c17d23..f0bba08bb8 100755
--- a/configure
+++ b/configure
@@ -749,6 +749,7 @@ build_os
build_vendor
build_cpu
build
+naked_pointers
compute_deps
stdlib_manpages
PACKLD
@@ -2907,6 +2908,7 @@ VERSION=4.12.0+dev0-2020-04-22
+
## Generated files
ac_config_files="$ac_config_files Makefile.build_config"
@@ -16863,8 +16865,11 @@ fi
## No naked pointers
if test x"$enable_naked_pointers" = "xno" ; then :
- $as_echo "#define NO_NAKED_POINTERS 1" >>confdefs.h
+ naked_pointers=false
+ $as_echo "#define NO_NAKED_POINTERS 1" >>confdefs.h
+else
+ naked_pointers=true
fi
## Check for mmap support for huge pages and contiguous heap