From 35ff66308bee60f5c0e0e917a8ad4b817bc36851 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Jul 2014 16:10:30 +0200 Subject: Coqide: annoying popups with GTK errors only in debug mode --- ide/coqide_main.ml4 | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'ide/coqide_main.ml4') diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index aad70197e..03aa9b754 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -33,7 +33,9 @@ let catch_gtk_messages () = |`FATAL -> let () = GToolbox.message_box ~title:"Error" (header ^ msg) in Coqide.crash_save 1 - |`ERROR -> GToolbox.message_box ~title:"Error" (header ^ msg) + |`ERROR -> + if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg) + else Printf.eprintf "%s\n" (header ^ msg) |`DEBUG -> Minilib.log msg |level when Sys.os_type = "Win32" -> Minilib.log ~level msg |_ -> Printf.eprintf "%s\n" msg -- cgit v1.2.3