From c9f0c0f4725533ee2294d416be82ca45dda2cabb Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 23 May 2012 15:21:17 +0000
Subject: Cleaned prerr_endline use.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/minilib.mli | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'ide/minilib.mli')

diff --git a/ide/minilib.mli b/ide/minilib.mli
index 1254f5a6d..c84321211 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -9,10 +9,16 @@
 (** Some excerpts of Util and similar files to avoid depending on them
     and hence on Compat and Camlp4 *)
 
+type level = [
+  | `DEBUG
+  | `INFO
+  | `NOTICE
+  | `WARNING
+  | `ERROR
+  | `FATAL ]
+
 (** debug printing *)
 val debug : bool ref
-val prerr_endline : string -> unit
 
-(** safe version of Pervasives.prerr_endline
-    (avoid exception in win32 without console) *)
-val safe_prerr_endline : string -> unit
+val log : ?level:level -> string -> unit
+
-- 
cgit v1.2.3