diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-04 16:00:06 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-04 16:00:06 +0000 |
commit | 2814afbbd4803216ad4cb6af9ec5d86fce71e8eb (patch) | |
tree | c764ff83abf5848046576c0c9d08d64c513ef447 /configure | |
parent | 5a4cc30c737f113a7c57d14569137b3e06f5639f (diff) |
Test make 3.81
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10754 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 34 |
1 files changed, 34 insertions, 0 deletions
@@ -290,6 +290,40 @@ else checkedout=0 fi +# make command + +MAKE=`which make` +if [ "$MAKE" != "" ]; then + MAKEVERSION=`$MAKE -v | head -1` + case $MAKEVERSION in + "GNU Make 3.81") + echo "You have GNU Make 3.81. Good!";; + *) + OK="no" + if [ -x ./make ]; then + MAKEVERSION=`./make -v | head -1` + if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi + fi + if [ $OK = "no" ]; then + echo "GNU Make >= 3.81 is needed" + echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz" + echo "then locally installed on a Unix-style system by issuing:" + echo " tar xzvf make-3.81.tar.gz" + echo " cd make-3.81" + echo " ./configure" + echo " make" + echo " mv make .." + echo " cd .." + echo "Restart then the configure script and later use ./make instead of make" + exit 1 + else + echo "You have locally installed GNU Make 3.81. Good!" + fi + esac +else + echo "Cannot find GNU Make 3.81" +fi + ######################################### # Objective Caml programs |