From bfa9987d57cd729c40332202a505753beca52e91 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 9 May 2016 15:32:18 +0200
Subject: 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.
---
 configure.ml | 19 +++----------------
 1 file changed, 3 insertions(+), 16 deletions(-)

(limited to 'configure.ml')

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, ... *)
-- 
cgit v1.2.3


From b43956fe19177a178dfbcef0b173ebada5060973 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 9 May 2016 15:32:38 +0200
Subject: Fix typo in configure's option description.

---
 configure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'configure.ml')

diff --git a/configure.ml b/configure.ml
index ff6c367c6..3fcc24d05 100644
--- a/configure.ml
+++ b/configure.ml
@@ -335,7 +335,7 @@ let args_options = Arg.align [
   "-coqwebsite", Arg.Set_string Prefs.coqwebsite,
     " URL of the coq website";
   "-force-caml-version", Arg.Set Prefs.force_caml_version,
-    "Force OCaml version";
+    " Force OCaml version";
 ]
 
 let parse_args () =
-- 
cgit v1.2.3