aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
diff options
context:
space:
mode:
authorPierre Roux2019-11-25 14:01:41 +0100
committerPierre Roux2019-11-26 16:06:56 +0100
commitf052f19f4b6f2603daebe5e6eae9daffd9cc008c (patch)
tree1b34f275b16264b2b173fb313195f7ae38144b00 /configure.ml
parent0e9cd0fe99216bc09a09a0da6906f9501b682223 (diff)
Fix Windows 32 bit build
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/configure.ml b/configure.ml
index 60ba8b1101..d4521a7872 100644
--- a/configure.ml
+++ b/configure.ml
@@ -919,16 +919,16 @@ let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s
let cflags_dflt = "-Wall -Wno-unused -g -O2 -fexcess-precision=standard"
-let cflags_sse2 = ["-msse2"; "-mfpmath=sse"]
+let cflags_sse2 = "-msse2 -mfpmath=sse"
let cflags, sse2_math =
let _, slurp =
(* Test SSE2_MATH support <https://stackoverflow.com/a/45667927> *)
- tryrun "cc" (["-march=native"; "-dM"; "-E"]
- @ cflags_sse2
- @ [coqtop/"kernel/byterun/coq_interp.h"] (* any file *)) in
+ tryrun camlexec.find
+ ["ocamlc"; "-ccopt"; cflags_dflt ^ " -march=native -dM -E " ^ cflags_sse2;
+ "-c"; coqtop/"dev/header.c"] in (* any file *)
if List.exists (fun line -> starts_with line "#define __SSE2_MATH__ 1") slurp
- then (cflags_dflt ^ " " ^ String.concat " " cflags_sse2, true)
+ then (cflags_dflt ^ " " ^ cflags_sse2, true)
else (cflags_dflt, false)
(** Test at configure time that no harmful double rounding seems to