]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitacLib.ml
changed .moo format on disk: no longer plain strings, but ocaml marshalling of Grafit...
[helm.git] / helm / matita / matitacLib.ml
index b30a55234b94f12d80c6330eefac65bba5de2636..48a2f2f9ec5d23d109c01be91defd94a32b6f12a 100644 (file)
@@ -159,11 +159,7 @@ let go () =
 
 let dump_moo_to_file file moo =
  let os = open_out (MatitaMisc.obj_file_of_script file) in
- let output s = output_string os s in
- output "(* GENERATED FILE: DO NOT EDIT! *)\n\n";
- List.iter
-  (fun cmd -> output (GrafiteAstPp.pp_command cmd ^ "\n"))
-  (List.rev moo);
+ Marshal.to_channel os (List.rev moo) [];
  close_out os
   
 let main ~mode =