X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;fp=helm%2Fmatita%2FmatitaGui.ml;h=74913dbe6d46c596cc73ecb640e93ac218c27e28;hb=3ce38077e0b1e2a38ad513d3c108d7ef3c09bb7c;hp=6b4afa3cf3e549f9f484ed54c71d14504750965e;hpb=dbb9f64a437b4abda0b9f47a527ab6135d596e28;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 6b4afa3cf..74913dbe6 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -72,8 +72,10 @@ let ask_and_save_moo_if_needed parent fname status =
   let basedir = Helm_registry.get "matita.basedir" in
   let save () =
     let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
-     GrafiteMarshal.save_moo moo_fname
-      status.GrafiteTypes.moo_content_rev in
+    let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in
+    GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev;
+    LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata
+  in
   if (MatitaScript.current ())#eos &&
      status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
   then