aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-05-09 15:32:18 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-05-09 15:32:18 +0200
commitbfa9987d57cd729c40332202a505753beca52e91 (patch)
tree8c68d9c69f7775b1438a2bf1c0467b1fa4d9ba6c /configure.ml
parent213e86842db2cdc3acc8cdf6d28f46c7ebaec5d4 (diff)
Use "md5 -q" on FreeBSD architectures (bug #4719).
This patch also disables the -makecmd option and the corresponding test, since the value is not stored for future use. This prevents gratuitously failing to configure on FreeBSD.
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml19
1 files changed, 3 insertions, 16 deletions
diff --git a/configure.ml b/configure.ml
index 9fdd451f1..ff6c367c6 100644
--- a/configure.ml
+++ b/configure.ml
@@ -251,7 +251,6 @@ module Prefs = struct
let debug = ref false
let profile = ref false
let annotate = ref false
- let makecmd = ref "make"
let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
let coqwebsite = ref "http://coq.inria.fr/"
let force_caml_version = ref false
@@ -329,8 +328,8 @@ let args_options = Arg.align [
" Add profiling information in the Coq executables";
"-annotate", Arg.Set Prefs.annotate,
" Dumps ml annotation files while compiling Coq";
- "-makecmd", Arg.Set_string Prefs.makecmd,
- "<command> Name of GNU Make command";
+ "-makecmd", Arg.String (fun _ -> printf "Warning: obsolete -makecmd option\n"),
+ "<command> Obsolete: name of GNU Make command";
"-native-compiler", arg_bool Prefs.nativecompiler,
"(yes|no) Compilation to native code for conversion and normalization";
"-coqwebsite", Arg.Set_string Prefs.coqwebsite,
@@ -447,18 +446,6 @@ let vcs =
else if dir_exists "{arch}" then "gnuarch"
else "none"
-(** * The make command *)
-
-let make =
- try
- let version_line, _ = run !Prefs.makecmd ["-v"] in
- let version = List.nth (string_split ' ' version_line) 2 in
- match string_split '.' version with
- | major::minor::_ when (s2i major, s2i minor) >= (3,81) ->
- printf "You have GNU Make %s. Good!\n" version
- | _ -> failwith "bad version"
- with _ -> die "Error: Cannot find GNU Make >= 3.81."
-
(** * Browser command *)
let browser =
@@ -851,7 +838,7 @@ let strip =
(** * md5sum command *)
let md5sum =
- if arch = "Darwin" then "md5 -q" else "md5sum"
+ if arch = "Darwin" || arch = "FreeBSD" then "md5 -q" else "md5sum"
(** * Documentation : do we have latex, hevea, ... *)