Correction du bug #2142

Ajout d'un test d'existence de pngtopnm et de pnmtops dans le
./configure

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12471 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 9 deletions

diff --git a/configure b/configure
index 245cf2b1a..2beecd6ff 100755
--- a/configure
+++ b/configure
@@ -670,17 +670,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
 
 ###########################################