aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-05-05 00:20:54 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-05-05 00:20:54 +0200
commit34e6a7149a69791cc736bdd9b2b909be9f21ec8f (patch)
treef33a4ed37d7fff96df7a720fe6146ecce56aba81 /configure.ml
parent72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (diff)
parentdf54c829a4c06a93de47df4e8ccc441721360da8 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/configure.ml b/configure.ml
index 3cf462ebe..267d556a2 100644
--- a/configure.ml
+++ b/configure.ml
@@ -27,7 +27,7 @@ let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1
let s2i = int_of_string
let i2s = string_of_int
-let (/) = Filename.concat
+let (/) x y = x ^ "/" ^ y
(** Remove the final '\r' that may exists on Win32 *)
@@ -396,8 +396,7 @@ let coq_annotate_flag =
then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes"
else ""
-let cflags = "-Wall -Wno-unused"
-
+let cflags = "-Wall -Wno-unused -g " ^ (if !Prefs.debug then "-O1" else "-O2")
(** * Architecture *)