]> matita.cs.unibo.it Git - helm.git/commitdiff
- simplified Makefile.defs using the ?= assignment
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 7 Sep 2015 15:03:43 +0000 (15:03 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 7 Sep 2015 15:03:43 +0000 (15:03 +0000)
- now the variable OCAMLPATH is available and is correctly set

matita/Makefile.defs.in

index d7a7620d5949bcfd9eb6cac398a823ad8843ec79..18c2549dc412a16926430db7c51497f33faea7c3 100644 (file)
@@ -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@