EXPERIMENTAL COMMIT (by CSC,actuall :-)

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index a4e879a36e985432df1ac7c16e3914702e924735..7580ebf2969545acb112ac0f2ca909bdc466feaa 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -274,6 +274,8 @@ let compile atstart options fname =
         (* FG: we do not generate .moo when dumping .mma files *)
         GrafiteMarshal.save_moo moo_fname moo_content_rev;
         LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+        NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri)
+         (GrafiteTypes.get_dump grafite_status)
      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in