From 05963c3c472ae13fbc9f5f80bd0fe2a616390340 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Jun 2005 09:01:54 +0000
Subject: [PATCH] fix

---
 helm/matita/matitaGtkMisc.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 4af50ee12..038aa7fd1 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -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) () =
-- 
2.39.2