summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
commit300293c119981054c95182a90c829058530a6b6f (patch)
treed7303613741c5796b58ced7db24ec7203327dbb2 /configure
parent9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff)
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure21
1 files changed, 11 insertions, 10 deletions
diff --git a/configure b/configure
index 7cff4b97..8498bd70 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
#
##################################
-VERSION=8.3pl2
+VERSION=8.3pl3
VOMAGIC=08300
STATEMAGIC=58300
DATE=`LANG=C date +"%B %Y"`
@@ -321,11 +321,12 @@ fi
MAKE=`which 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"
if [ -x ./make ]; then
MAKEVERSION=`./make -v | head -1`
@@ -346,9 +347,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
@@ -659,7 +660,7 @@ esac
if test "$with_doc" = "all"
then
- for cmd in "latex" "hevea" "pngtopnm" "pnmtops" ; do
+ for cmd in "latex" "hevea" ; do
if test ! -x "`which $cmd`"
then
echo "$cmd was not found; documentation will not be available"
@@ -1084,4 +1085,4 @@ echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id: configure 14025 2011-04-19 07:19:00Z notin $
+# $Id: configure 14833 2011-12-19 21:57:30Z notin $