diff options
Diffstat (limited to 'devel/coq/0001-fix-make-detection.patch')
| -rw-r--r-- | devel/coq/0001-fix-make-detection.patch | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/devel/coq/0001-fix-make-detection.patch b/devel/coq/0001-fix-make-detection.patch new file mode 100644 index 0000000000..8c95f7798d --- /dev/null +++ b/devel/coq/0001-fix-make-detection.patch @@ -0,0 +1,61 @@ +From 5e3aadfd0f36fb95cf4bc45e819780883d4a541b Mon Sep 17 00:00:00 2001 +From: Florian Franzmann <siflfran@hawo.stw.uni-erlangen.de> +Date: Sun, 2 Feb 2014 00:39:39 +0100 +Subject: [PATCH] fix make detection + +--- + configure | 20 ++++++++++---------- + 1 file changed, 10 insertions(+), 10 deletions(-) + +diff --git a/configure b/configure +index 7f75b35..d99340a 100755 +--- a/configure ++++ b/configure +@@ -336,22 +336,22 @@ 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" -eq 4 -a "$MAKEVERSIONMINOR" -ge 0 ]; 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 ++ #Extra support for local installation of make 4.0 ++ #will be useless when make >= 4.0 will be standard + if [ -x ./make ]; then + MAKEVERSION=`./make -v | head -1` +- if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi ++ if [ "$MAKEVERSION" = "GNU Make 4.0" ]; 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 "GNU Make >= 4.0 is needed." ++ echo "Make 4.0 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-4.0.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 " tar xzvf make-4.0.tar.gz" ++ echo " cd make-4.0" + echo " ./configure" + echo " make" + echo " mv make .." +@@ -359,11 +359,11 @@ if [ "$MAKE" != "" ]; then + 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!" ++ echo "You have locally installed GNU Make 4.0. Good!" + fi + fi + else +- echo "Cannot find GNU Make >= 3.81." ++ echo "Cannot find GNU Make >= 4.0." + fi + + # Browser command +-- +1.8.5.3 + |