X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitacLib.ml;h=17e83c976baf2d4268b80a2a5b25bca4d3a5dced;hb=25b60c359f88d29e7f0b916c95cafc1cab06dc5b;hp=17cb2952c08a879c874566c2aea693fc5a191dc2;hpb=b49a7265f5da01f89b5c845f52b31c2f728cc293;p=helm.git

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 17cb2952c..17e83c976 100644
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -335,10 +335,10 @@ 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,metadata,lexicon_content_rev = 
+    let proof_status,moo_content_rev,lexicon_content_rev = 
       match !lexicon_status,!grafite_status with
       | Some ss, Some s ->
-         s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
+         s.proof_status, s.moo_content_rev, 
           ss.LexiconEngine.lexicon_content_rev
       | _,_ -> assert false
     in
@@ -361,12 +361,7 @@ let main ~mode =
          LibraryMisc.lexicon_file_of_baseuri 
           ~must_exist:false ~baseuri ~writable:true 
        in
-       let metadata_fname =
-        LibraryMisc.metadata_file_of_baseuri 
-          ~must_exist:false ~baseuri ~writable:true
-       in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
-       LibraryNoDb.save_metadata metadata_fname metadata;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
        HLog.message 
          (sprintf "execution of %s completed in %s." fname (hou^min^sec));