From 8866d53c2f6f93a012062817ef0a4e4e4eb6997b Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 5 Nov 2009 16:11:11 +0000
Subject: 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
---
 configure | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/configure b/configure
index 245cf2b1ab..2beecd6ff1 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
 
 ###########################################
-- 
cgit v1.2.3