diff options
Diffstat (limited to 'ide/minilib.mli')
| -rw-r--r-- | ide/minilib.mli | 14 |
1 files changed, 10 insertions, 4 deletions
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 + |