X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=27147e6d422ec184112bbecf5a0b118a22440e7f;hb=3174ea6822b2adc68be84428c883e240b5281433;hp=de89752151952761eac0edb23be21fb1b7b61d42;hpb=5228acfa3e0e37019dac156ba85434b83e8f469d;p=helm.git

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index de8975215..27147e6d4 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -120,21 +120,13 @@ let rec interactive_loop () =
   | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop ()
 
 let go () =
-  Helm_registry.load_from "matita.conf.xml";
+  Helm_registry.load_from BuildTimeConf.matita_conf;
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
   status := Some (ref (Lazy.force MatitaEngine.initial_status));
   Sys.catch_break true;
   interactive_loop ()
 
-let clean_exit n =
- match !status with
-    None -> exit n
-  | Some status ->
-     let baseuri = MatitaTypes.get_string_option !status "baseuri" in
-      MatitacleanLib.clean_baseuris ~verbose:false [baseuri];
-      exit n
-  
 let dump_moo_to_file file moo =
  let os = open_out (MatitaMisc.obj_file_of_script file) in
  let output s = output_string os s in
@@ -143,9 +135,10 @@ let dump_moo_to_file file moo =
  close_out os
   
 let main ~mode = 
-  Helm_registry.load_from "matita.conf.xml";
+  Helm_registry.load_from BuildTimeConf.matita_conf;
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+  MatitaDb.create_owner_environment ();
   status := Some (ref (Lazy.force MatitaEngine.initial_status));
   Sys.catch_break true;
   let fname = fname () in