- 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;