From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 7 Sep 2015 15:03:43 +0000 (+0000)
Subject: - simplified Makefile.defs using the ?= assignment
X-Git-Tag: make_still_working~695
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e2922190ff27bd32da8d3bb7ca9aba8cd5cb6b8a;p=helm.git

- simplified Makefile.defs using the ?= assignment
- now the variable OCAMLPATH is available and is correctly set
---

diff --git a/matita/Makefile.defs.in b/matita/Makefile.defs.in
index d7a7620d5..18c2549dc 100644
--- a/matita/Makefile.defs.in
+++ b/matita/Makefile.defs.in
@@ -1,8 +1,5 @@
-ifeq ($(origin OCAMLPATH), undefined)
-OCAMLFIND = OCAMLPATH=@OCAMLPATH@ @OCAMLFIND@
-else
-OCAMLFIND = @OCAMLFIND@
-endif
+OCAMLPATH ?= @OCAMLPATH@
+OCAMLFIND = OCAMLPATH=$(OCAMLPATH) @OCAMLFIND@
 CAMLP5O = @CAMLP5O@
 LABLGLADECC = @LABLGLADECC@
 HAVE_OCAMLOPT = @HAVE_OCAMLOPT@