fixed some errers in the save/cancel ...

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index fa6059d1ea0eebb8139ac900f86e767074daeacd..b21c3b340e4ea0ce383993228179dd1ee151f393 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -262,7 +262,9 @@ class gui () =
                 ()
             in
             match rc with
-            | `YES -> saveScript ();GMain.Main.quit ()
+            | `YES -> saveScript ();
+                      if not source_view#buffer#modified then
+                        GMain.Main.quit ()
             | `NO -> GMain.Main.quit ()
             | `CANCEL -> ()
           end else GMain.Main.quit ());