]> matita.cs.unibo.it Git - helm.git/commitdiff
fix
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 29 Jun 2005 09:01:54 +0000 (09:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 29 Jun 2005 09:01:54 +0000 (09:01 +0000)
helm/matita/matitaGtkMisc.ml

index 4af50ee12393281c3c14cc1b510715e3c4dd2718..038aa7fd13539a0cf7d1a6575d36dfa6628f556e 100644 (file)
@@ -207,12 +207,11 @@ let report_error ~title ~message ?parent () =
   let rc = ref false in
   let callback _ = () in
   let buttons = GWindow.Buttons.ok in
-(  try 
+  try 
     popup_message ~title ~message ~message_type:`ERROR ~callback ~buttons 
     ?parent ()
   with
   | PopupClosed -> ()
-);prerr_endline "AAAAAAA" 
 
 
 let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =