X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=b901908207b19624ff63346434d33d3fe98c684a;hb=6b38b8f5c675570ca5a70e917cf77c783ef2d092;hp=55c5f2a02318f66b9f66601a882cc3e41e9141bc;hpb=ebe70c001a623e0440f21cd16dc88f585edcf0ea;p=helm.git

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 55c5f2a02..b90190820 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -170,9 +170,9 @@ let main ~mode =
     let hou = 
       if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
     in
-    let proof_status,moo_content_rev,status = 
+    let proof_status,moo_content_rev,metadata,status = 
       match !status with
-      | Some s -> !s.proof_status, !s.moo_content_rev, !s
+      | Some s -> !s.proof_status, !s.moo_content_rev, !s.metadata, !s
       | None -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
@@ -185,7 +185,9 @@ let main ~mode =
      begin
        let basedir = Helm_registry.get "matita.basedir" in
        let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
+       let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
+       LibraryNoDb.save_metadata metadata_fname metadata;
        HLog.message 
          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
        exit 0