From 40d0bc5a5fecd61bc4189891f5c427f7b328b450 Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 3 Nov 2013 20:33:03 +0000
Subject: configure stript allows make v4.00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17042 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 configure | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'configure')

diff --git a/configure b/configure
index 273ab045b..5f91aa1f6 100755
--- a/configure
+++ b/configure
@@ -339,7 +339,7 @@ if [ "$MAKE" != "" ]; then
   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
+  if [ "$MAKEVERSIONMAJOR" -gt 3 -o "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
       echo "You have GNU Make $MAKEVERSION. Good!"
   else
       OK="no"
-- 
cgit v1.2.3