From bf7be462a06e739b39af20f72362857e849a2aa0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 5 Jan 2018 21:17:18 +0100 Subject: [PATCH] matita.basedir used consistently --- matita/matita/matita.conf.xml.in | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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