Large commit:

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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 13db5d2760a36216344c84676041cbad71b0b960..17d299eaebedaf0965b2b7b8315c4253beffac81 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -76,7 +76,7 @@ let save_moo grafite_status =
   | true, _ -> ()
   | _, true ->
      GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
-      ~dependencies:grafite_status#dependencies grafite_status#dump
+      grafite_status
   | _ -> clean_current_baseuri grafite_status 
 ;;