maxipatch for support of multiple DBs.

[helm.git] / helm / software / matita / matitaWiki.ml

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index c7c5e8838c74defd6a6687aa0b6b938e866a39c5..bbe8d2ed7247f60132ffa0f97e4c7e298959efc9 100644 (file)
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -231,10 +231,10 @@ let main () =
       | End_of_file -> ()
       | GrafiteEngine.Drop -> clean_exit 1
     );
-    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
       | ss::_, 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
@@ -259,12 +259,7 @@ let main () =
          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;
        exit 0
      end