diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 25 |
1 files changed, 11 insertions, 14 deletions
@@ -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 $ |