Dead code for .moo files removed.

[helm.git] / matita / matita / matitaGui.ml

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 6f4e09bbc6e2d29e01e3c76776c1d5852401f6a0..6d4c8c0f5601173583b9c36d4e1969df086def4b 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -75,14 +75,10 @@ let save_moo grafite_status =
   match script#bos, script#eos with
   | true, _ -> ()
   | _, true ->
-     let moo_fname = 
-       LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
-        ~writable:true in
      let lexicon_fname =
        LibraryMisc.lexicon_file_of_baseuri 
          ~must_exist:false ~baseuri ~writable:true
      in
-     GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
      LexiconMarshal.save_lexicon lexicon_fname
       grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
      NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)