aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-07-18 12:18:05 +0200
committerPierre-Marie Pédrot2015-07-18 12:18:05 +0200
commit88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch)
tree01f750142359361f800e0dc2dfe422f145f491c5 /configure.ml
parent139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff)
parentfdd6a17b272995237c9f95fc465bb1ff6871bedc (diff)
Merge branch 'v8.5'
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index a1c172cf48..83468f8f34 100644
--- a/configure.ml
+++ b/configure.ml
@@ -372,7 +372,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 *)