aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-09-17 09:48:19 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-09-17 09:48:19 +0200
commit13ea0a5011875e362aa388989b72b3f7ed0c505b (patch)
treefaa045035065875845cea1c80cbb3a3b4f624fbf /configure.ml
parentf2f805ed8275f70767284f4d3c8a13db6f8c8923 (diff)
parentfbb3ccdb099170e5a39c9f39512b1ab2503951ea (diff)
Merge branch 'v8.5' into trunk
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/configure.ml b/configure.ml
index ffb7c15f5..7e0d68eb8 100644
--- a/configure.ml
+++ b/configure.ml
@@ -252,7 +252,7 @@ module Prefs = struct
let profile = ref false
let annotate = ref false
let makecmd = ref "make"
- let nativecompiler = ref true
+ let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
let coqwebsite = ref "http://coq.inria.fr/"
let force_caml_version = ref false
end
@@ -331,8 +331,8 @@ let args_options = Arg.align [
" Dumps ml annotation files while compiling Coq";
"-makecmd", Arg.Set_string Prefs.makecmd,
"<command> Name of GNU Make command";
- "-no-native-compiler", Arg.Clear Prefs.nativecompiler,
- " No compilation to native code for conversion and normalization";
+ "-native-compiler", arg_bool Prefs.nativecompiler,
+ " (yes|no) Compilation to native code for conversion and normalization";
"-coqwebsite", Arg.Set_string Prefs.coqwebsite,
" URL of the coq website";
"-force-caml-version", arg_bool Prefs.force_caml_version,