]> matita.cs.unibo.it Git - helm.git/commitdiff
we always update OCAMLPATH rather than leaving it unchanged if defined
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 31 Mar 2017 12:34:49 +0000 (12:34 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 31 Mar 2017 12:34:49 +0000 (12:34 +0000)
matita/Makefile.defs.in

index 18c2549dc412a16926430db7c51497f33faea7c3..90a203f738c8ccec2480f35ceaa751a63c85e908 100644 (file)
@@ -1,4 +1,4 @@
-OCAMLPATH ?= @OCAMLPATH@
+OCAMLPATH := @OCAMLPATH@:$(OCAMLPATH)
 OCAMLFIND = OCAMLPATH=$(OCAMLPATH) @OCAMLFIND@
 CAMLP5O = @CAMLP5O@
 LABLGLADECC = @LABLGLADECC@