aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJason Gross2020-03-27 16:50:08 -0400
committerJason Gross2020-03-27 16:50:08 -0400
commit28081c1108a84050566d365bd665d05ee508ecce (patch)
tree6c6dd426b7d4bfe33b1801e658445cbaf8e4eac0
parent974915a91a03199a8151eddf8ffce9a270da2d77 (diff)
parenta5ef6f5b8c73f59d4dc26754149daddc41cf65f5 (diff)
Merge PR #11809: [configure] Remove `-std=c99` from default C flags
Reviewed-by: JasonGross Ack-by: SkySkimmer
-rw-r--r--configure.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 55d71f6c2e..ee2e50ef86 100644
--- a/configure.ml
+++ b/configure.ml
@@ -923,7 +923,11 @@ let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s
(** * CC runtime flags *)
-let cflags_dflt = "-Wall -Wno-unused -g -O2 -std=c99 -fasm"
+(* Note that Coq's VM requires at least C99-compliant floating-point
+ arithmetic; this should be ensured by OCaml's own C flags, which
+ set a minimum of [--std=gnu99] ; modern compilers by default assume
+ C11 or later, so no explicit [--std=] flags are added by OCaml *)
+let cflags_dflt = "-Wall -Wno-unused -g -O2"
let cflags_sse2 = "-msse2 -mfpmath=sse"