Add -makecmd configure option

This allows choosing gmake on *BSD (patch from Nima Hoda).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12689 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 1 deletions

diff --git a/configure b/configure
index fad222fdb..c3aaa241a 100755
--- a/configure
+++ b/configure
@@ -85,6 +85,8 @@ usage () {
     printf "\tAdd profiling information in the Coq executables\n"
     echo "-annotate"
     printf "\tCompiles Coq with -dtypes option\n"
+    echo "-makecmd <command>"
+    printf "\tName of GNU Make command.\n"
 }
 
 
@@ -239,6 +241,8 @@ while : ; do
 	  ranlib_spec=yes
 	  ranlib_exec=$2
 	  shift;;
+    -makecmd|--makecmd) makecmd="$2"
+		      shift;;
     -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
     -debug|--debug) coq_debug_flag=-g;;
     -profile|--profile) coq_profile_flag=-p;;
@@ -319,7 +323,7 @@ fi
 
 # make command
 
-MAKE=`which make`
+MAKE=`which ${makecmd:-make}`
 if [ "$MAKE" != "" ]; then
   MAKEVERSION=`$MAKE -v | head -1`
   case $MAKEVERSION in