metadata are no longer stored in .moo files.

[helm.git] / helm / matita / matitacLib.ml

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 55c5f2a02318f66b9f66601a882cc3e41e9141bc..b901908207b19624ff63346434d33d3fe98c684a 100644 (file)
--- 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