]> matita.cs.unibo.it Git - helm.git/commitdiff
removed "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 2 Feb 2006 16:22:23 +0000 (16:22 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 2 Feb 2006 16:22:23 +0000 (16:22 +0000)
if it will be needed in the future it should be implemented (properly) in the
registry itself

helm/matita/matitaInit.ml

index 8223416e4dd7d632846e7963927bef57e700948e..34b64284f85f3f0f99f7bbb13ae0b4cf5da1ddad 100644 (file)
@@ -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