diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-09 15:32:18 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-09 15:32:18 +0200 |
commit | bfa9987d57cd729c40332202a505753beca52e91 (patch) | |
tree | 8c68d9c69f7775b1438a2bf1c0467b1fa4d9ba6c /configure.ml | |
parent | 213e86842db2cdc3acc8cdf6d28f46c7ebaec5d4 (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.ml | 19 |
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, ... *) |