Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg

1 files changed, 11 insertions, 14 deletions

diff --git a/configure b/configure
index 1ba4eaba..db7a55a0 100755
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/sh
 
 ##################################
 #
@@ -6,7 +6,7 @@
 # 
 ##################################
 
-VERSION=8.2pl1
+VERSION=8.2pl2
 VOMAGIC=08200
 STATEMAGIC=58200
 DATE=`LANG=C date +"%B %Y"`
@@ -331,7 +331,7 @@ if [ "$MAKE" != "" ]; then
       OK="no"
       if [ -x ./make ]; then
 	  MAKEVERSION=`./make -v | head -1`
-	  if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi
+	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
       fi
       if [ $OK = "no" ]; then
 	  echo "GNU Make >= 3.81 is needed"
@@ -363,7 +363,7 @@ if [ "$browser_spec" = "no" ]; then
 fi
 
 if [ "$wwwcoq_spec" = "no" ]; then
-    WWWCOQ="http://www.lix.polytechnique.fr/coq/"
+    WWWCOQ="http://coq.inria.fr/"
 fi
 
 #########################################
@@ -665,17 +665,14 @@ esac
 
 if test "$with_doc" = "all" 
 then
-    if test "`which latex`" = ""
-    then 
-	echo "latex was not found; documentation will not be available"
-	with_doc=no
-    else
-	if test "`which hevea`" = ""
-	then
+    for cmd in "latex" "hevea" "pngtopnm" "pnmtops" ; do
+	if test ! -x "`which $cmd`"
+	then 
+	    echo "$cmd was not found; documentation will not be available"
 	    with_doc=no
-	    echo "hevea was not found: documentation will not be available"
+	    break
 	fi
-    fi
+    done
 fi
 
 ###########################################
@@ -1080,4 +1077,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 12219 2009-07-01 09:58:00Z notin $
+# $Id: configure 13223 2010-06-29 18:28:35Z notin $