X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=5ed1d41b443e5b56d6a3355e0593b12da6de5595;hb=8de1a75899a83dd31e856804bd448c1bd87d9ab3;hp=1f880575e063860d85663f711e5390babf74e258;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 1f880575e..5ed1d41b4 100644
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -222,11 +222,12 @@ let main () =
       | End_of_file -> ()
       | GrafiteEngine.Drop -> clean_exit 1
     );
-    let proof_status,moo_content_rev,lexicon_content_rev = 
+    let proof_status,moo_content_rev,lexicon_content_rev,dump = 
       match !grafite_status with
       |  s::_ ->
          s.proof_status, s.moo_content_rev,
-          (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev
+          (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev,
+          GrafiteTypes.get_dump s
       | _ -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
@@ -253,6 +254,7 @@ let main () =
        in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+       NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
        exit 0
      end
   with