From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 2 Feb 2006 16:22:23 +0000 (+0000)
Subject: removed "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
X-Git-Tag: make_still_working~7674
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c4eec8df32b6b004e76cbce54342385d3bf25fa5;p=helm.git

removed "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
if it will be needed in the future it should be implemented (properly) in the
registry itself
---

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 8223416e4..34b64284f 100644
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -42,11 +42,6 @@ let wants s l =
 let already_configured s l =
   List.for_all (fun item -> List.exists (fun x -> x = item) l) s
   
-let tilde_expand_key k =
-  try
-    Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
-  with Helm_registry.Key_not_found _ -> ()
-
 let load_configuration init_status =
   if not (already_configured [ConfigurationFile] init_status) then
     begin
@@ -55,12 +50,8 @@ let load_configuration init_status =
         let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
         Helm_registry.set "user.name" login
       end;
-      tilde_expand_key "matita.basedir";
-      if Helm_registry.get_bool "matita.system" then begin
-        prerr_endline "SISTEMA";
+      if Helm_registry.get_bool "matita.system" then
         Helm_registry.set "user.home" BuildTimeConf.runtime_base_dir;
-      end;
-      tilde_expand_key "user.home";
       ConfigurationFile::init_status 
     end
   else