X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=7decc583c58ab4b8de1b7a0dab4b49867792bae9;hb=e362056c17a503d3ac47600db90de1c534fb1fbb;hp=e2274c387162f7b4830c104c0764706406058850;hpb=ee3f8d6fa92b051394a2ff7c71c03ac33a05182b;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index e2274c387..7decc583c 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -71,12 +71,15 @@ let clean_current_baseuri grafite_status =
 
 let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = 
   let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in
-  let moo_fname = LibraryMisc.obj_file_of_baseuri ~baseuri ~writable:true in
+  let moo_fname = 
+    LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in
   let save () =
     let metadata_fname =
-     LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true in
+     LibraryMisc.metadata_file_of_baseuri 
+       ~must_exist:false ~baseuri ~writable:true in
     let lexicon_fname =
-     LibraryMisc.lexicon_file_of_baseuri ~baseuri ~writable:true
+     LibraryMisc.lexicon_file_of_baseuri 
+       ~must_exist:false ~baseuri ~writable:true
     in
      GrafiteMarshal.save_moo moo_fname
       grafite_status.GrafiteTypes.moo_content_rev;