From c4eec8df32b6b004e76cbce54342385d3bf25fa5 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 16:22:23 +0000 Subject: [PATCH] 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 --- helm/matita/matitaInit.ml | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) 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 -- 2.39.5