Quit without saving dialog fixed

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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 4dc6274a38742f5123b31c04dc924c00c0e2c608..ee268e60add67ea6c06217317c37ebcefc340e90 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -931,7 +931,7 @@ class gui () =
              save_moo script#status;
              true
         | `NO -> true
-        | `CANCEL -> false
+        | `DELETE_EVENT -> false
       else 
        (save_moo script#status; true)