From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 11 Jul 2005 14:36:05 +0000 (+0000)
Subject: default USER_HOME to pwd
X-Git-Tag: pre_notation~38
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f508a0d1a9202186ec9b913ce1ddc6861918ad64;p=helm.git

default USER_HOME to pwd
---

diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac
index 293d8a767..a530cae56 100644
--- a/helm/matita/configure.ac
+++ b/helm/matita/configure.ac
@@ -90,7 +90,7 @@ if test "$DEBUG" = "true"; then
 fi
 
 RT_BASE_DIR=`pwd`
-USER_HOME=`echo $HOME`
+USER_HOME=`pwd` #should be `echo $HOME`
 USER_NAME=`echo $USER`
 
 AC_SUBST(CAMLP4O)