diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:17 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:17 +0200 |
commit | 2dad86a4e71bae9905b39970384328316e53eb42 (patch) | |
tree | 9fe7df673a3e36cfbee14f2a4afe5b5b6fc72e80 /configure | |
parent | 257f04de91e394cea67254da547fc1b90fa6978d (diff) | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Merge commit 'upstream/8.2pl2+dfsg'
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 $ |