diff options
| author | Emilio Jesus Gallego Arias | 2020-03-11 21:31:06 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-27 13:56:31 -0400 |
| commit | a5ef6f5b8c73f59d4dc26754149daddc41cf65f5 (patch) | |
| tree | 5c2e85a440a010c447d78465aaf24dc7424e17ab /configure.ml | |
| parent | bc500cd96c7142cda5ad6f992c7c656d6499b0c6 (diff) | |
[configure] Remove `-std=c99` from default C flags
Recent OCaml don't allow to build the VM with `--std=c99` anymore due
to changes in header files. `gnu99` is required, but it turns out this
is already enforced by OCaml, so we just remove the flag altogether.
See the discussion in #11432
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 6 |
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" |