From: Ferruccio Guidi Date: Fri, 5 Jan 2018 20:17:18 +0000 (+0100) Subject: matita.basedir used consistently X-Git-Tag: make_still_working~378 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bf7be462a06e739b39af20f72362857e849a2aa0 matita.basedir used consistently --- diff --git a/matita/matita/matita.conf.xml.in b/matita/matita/matita.conf.xml.in index aeb8af025..c16e997bb 100644 --- a/matita/matita/matita.conf.xml.in +++ b/matita/matita/matita.conf.xml.in @@ -77,7 +77,7 @@ Beware that this dir may become really space-consuming. It wont be used if all prefexises below are local (i.e. "file:///" URI scheme). --> - $(user.home)/.matita/getter/cache + $(matita.basedir)/getter/cache