diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-23 15:21:17 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-23 15:21:17 +0000 |
| commit | c9f0c0f4725533ee2294d416be82ca45dda2cabb (patch) | |
| tree | 2ec02034a35c0d3855f177e48ed0e09efa073362 /ide/minilib.mli | |
| parent | 8837c2365c382adb0a74bfedabb1659eeb472adc (diff) | |
Cleaned prerr_endline use.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
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 + |