From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 1 Jul 2010 17:21:14 +0200 Subject: Imported Upstream version 8.2pl2+dfsg --- configure | 25 +++++++++++-------------- 1 file changed, 11 insertions(+), 14 deletions(-) (limited to 'configure') 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 $ -- cgit v1.2.3