X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitacLib.ml;h=c2cdd7ef5787e886f9629ca8bb5bb7bf27677bf4;hb=6f2cc0ef8219ac6fd5b09a1f1fdc0bb5a2cc48cd;hp=8bb0dab4c2a1dd12af444535b0f10cf81e8a8376;hpb=c68d9805aa7e37554bc4f00eca61083b75ef43da;p=helm.git

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 8bb0dab4c..c2cdd7ef5 100644
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -371,8 +371,11 @@ let main ~mode =
          LibraryMisc.lexicon_file_of_baseuri 
           ~must_exist:false ~baseuri ~writable:true 
        in
-       GrafiteMarshal.save_moo moo_fname moo_content_rev;
-       LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+(* FG: we do not generate .moo when dumping .mma files *)
+       if Helm_registry.get_bool "matita.moo" then begin
+          GrafiteMarshal.save_moo moo_fname moo_content_rev;
+          LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+       end;
        HLog.message 
          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
        pp_times fname bench_mode true big_bang;