From ce7054e5eb47c5bf2bc569ef7af1b90fa7a00bca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 12 Oct 2011 15:30:54 +0000
Subject: Patch to support (a priori) all versions of make 3.xx >= 3.81

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14557 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 configure | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/configure b/configure
index f771c5e302..1d6b086f00 100755
--- a/configure
+++ b/configure
@@ -341,12 +341,15 @@ fi
 
 MAKE=`which ${makecmd:-make}`
 if [ "$MAKE" != "" ]; then
-  MAKEVERSION=`$MAKE -v | head -1`
-  case $MAKEVERSION in
-    "GNU Make 3.8"[12])
-      echo "You have GNU Make >= 3.81. Good!";;
-    *)
+  MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
+  MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
+  MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
+  if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
+      echo "You have GNU Make $MAKEVERSION. Good!"
+  else
       OK="no"
+      #Extra support for local installation of make 3.81
+      #will be useless when make >= 3.81 will be standard
       if [ -x ./make ]; then
 	  MAKEVERSION=`./make -v | head -1`
 	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
@@ -366,9 +369,9 @@ if [ "$MAKE" != "" ]; then
       else
 	  echo "You have locally installed GNU Make 3.81. Good!"
       fi
-  esac
+  fi
 else
-  echo "Cannot find GNU Make 3.81."
+  echo "Cannot find GNU Make >= 3.81."
 fi
 
 # Browser command
-- 
cgit v1.2.3