aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-05-02 10:13:37 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-05-02 10:13:37 +0000
commit8e6b8c82ea3b7b4afe9ad770f34c98359f71fb9a (patch)
treead340d7633101d8acf9538a22886f7c238d50819 /ide
parent8de001fbc2dd1a5fcec2bfd9d5fb5f022d4b77be (diff)
Affichage des warning gtk comme warning coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8776 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index a90f473c1..cc9268b91 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3358,7 +3358,10 @@ let start () =
ignore (
Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
`WARNING;`CRITICAL]
- (fun ~level msg -> failwith ("Coqide internal error: " ^ msg)));
+ (fun ~level msg ->
+ if level land Glib.Message.log_level `WARNING <> 0
+ then Pp.warning msg
+ else failwith ("Coqide internal error: " ^ msg)));
Command_windows.main ();
Blaster_window.main 9;
main files;