aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-05 16:11:11 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-05 16:11:11 +0000
commit8866d53c2f6f93a012062817ef0a4e4e4eb6997b (patch)
treeaa7db4945d583c7352865f38c00afabae5cd3f17 /configure
parent168b93bdd129877baecfe47ed5f6619cc10c10a5 (diff)
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
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure15
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
###########################################