From: Stefano Zacchiroli Date: Wed, 22 Jun 2005 13:50:50 +0000 (+0000) Subject: local use of OCAMLPATH so that ./script.sh should not be needed anymore X-Git-Tag: INDEXING_NO_PROOFS~100 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a01bd3bb2a1d7b891b6c8b024bf6975d86d2a1f;p=helm.git local use of OCAMLPATH so that ./script.sh should not be needed anymore --- diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index bbf534b32..1ace35ca4 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -1,5 +1,6 @@ -OCAMLFIND = @OCAMLFIND@ +OCAMLPATH = ../ocaml/METAS/ +OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@ CAMLP4O = @CAMLP4O@ LABLGLADECC = @LABLGLADECC@ REQUIRES = @FINDLIB_REQUIRES@ diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index e25e1c65c..745b4dfbe 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -48,7 +48,7 @@ helm-xmldiff \ for r in $FINDLIB_REQUIRES do AC_MSG_CHECKING(for $r ocaml library) - if $OCAMLFIND query $r &> /dev/null; then + if OCAMLPATH=../ocaml/METAS $OCAMLFIND query $r &> /dev/null; then AC_MSG_RESULT(yes) else AC_MSG_ERROR(could not find $r ocaml library)