aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2016-06-27 23:49:09 +0200
committerEmilio Jesus Gallego Arias2017-10-10 10:47:31 +0200
commit406717ce786a70e64b9043db45dd5a2add68f817 (patch)
treef37eeae1efcc765045ff1851cb79518cb23bf4e1 /tools
parentf927df44202034fa8cf73f72af876ae1e4ca05ba (diff)
[configure] Support for flambda flags.
We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
Diffstat (limited to 'tools')
-rw-r--r--tools/coqmktop.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index c21db300ad..950ed53ccf 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -32,6 +32,8 @@ let supported_suffix f = match CUnix.get_extension f with
| ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true
| _ -> false
+let supported_flambda_option f = List.mem f Coq_config.flambda_flags
+
(** From bytecode extension to native
*)
let native_suffix f = match CUnix.get_extension f with
@@ -187,6 +189,7 @@ let parse_args () =
end
| ("-h"|"-help"|"--help") :: _ -> usage ()
+ | f :: rem when supported_flambda_option f -> parse (op,fl) rem
| f :: rem when supported_suffix f -> parse (op,f::fl) rem
| f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1
in
@@ -275,7 +278,7 @@ let main () =
let prog = if !opt then "opt" else "ocamlc" in
(* Which arguments ? *)
if !opt && !top then failwith "no custom toplevel in native code!";
- let flags = if !opt then [] else Coq_config.vmbyteflags in
+ let flags = if !opt then Coq_config.flambda_flags else Coq_config.vmbyteflags in
let topstart = if !top then [ "topstart.cmo" ] else [] in
let (modules, tolink) = files_to_link userfiles in
let main_file = create_tmp_main_file modules in