diff options
| author | notin | 2006-09-14 16:10:47 +0000 |
|---|---|---|
| committer | notin | 2006-09-14 16:10:47 +0000 |
| commit | a782a2cea6803087ecf7e6a5bdf4696fb8a1c2f1 (patch) | |
| tree | 8f315370a9e289c2b1bdebee9ea919a1c2ce7dd2 | |
| parent | 6a06eabc8a035c94a42baf0b6cc27efb0f4b8ade (diff) | |
Bug dans configure (test best_compiler)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9139 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -330,7 +330,7 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"` # do we have a native compiler: test of ocamlopt and its version if [ "$best_compiler" = "opt" ] ; then - if test -e "$nativecamlc" ; then + if test -e `which "$nativecamlc"` ; then CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then echo "native and bytecode compilers do not have the same version!"; fi |