diff options
| author | Guillaume Melquiond | 2015-07-08 07:35:38 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-07-08 07:35:38 +0200 |
| commit | 6a0b36f13e9b9ebd693cc2b1688ace9905aa4042 (patch) | |
| tree | 156f91dc0ba882935d3ae50fc001d429ec038f45 | |
| parent | f29b968c54889dd82fd07d50bc6a52b63ea4edf0 (diff) | |
Use the same optimization level for the VM, whatever the debug level.
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 1916e82172..c759782d9d 100644 --- a/configure.ml +++ b/configure.ml @@ -396,7 +396,7 @@ let coq_annotate_flag = then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes" else "" -let cflags = "-Wall -Wno-unused -g " ^ (if !Prefs.debug then "-O1" else "-O2") +let cflags = "-Wall -Wno-unused -g -O2" (** * Architecture *) |