safe_prerr_endline in Minilib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14442 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 0 deletions

diff --git a/ide/minilib.ml b/ide/minilib.ml
index 2182c45e0..96d257df6 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -75,6 +75,15 @@ let home =
 let coqlib = ref ""
 let coqtop_path = ref ""
 
+(* On a Win32 application with no console, writing to stderr raise
+   a Sys_error "bad file descriptor", hence the "try" below.
+   Ideally, we should re-route message to a log file somewhere, or
+   print in the response buffer.
+*)
+
+let safe_prerr_endline s =
+  try prerr_endline s;flush stderr with _ -> ()
+
 (* Hints to partially detects if two paths refer to the same repertory *)
 let rec remove_path_dot p =
   let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)