diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-05 00:20:54 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-05 00:20:54 +0200 |
commit | 34e6a7149a69791cc736bdd9b2b909be9f21ec8f (patch) | |
tree | f33a4ed37d7fff96df7a720fe6146ecce56aba81 /configure.ml | |
parent | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (diff) | |
parent | df54c829a4c06a93de47df4e8ccc441721360da8 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'configure.ml')
-rw-r--r-- | configure.ml | 5 |
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 *) |