diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index f15cd120c..fe8936877 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -30,8 +30,12 @@ val is_char_start : char -> bool val lib_ide_file : string -> string val my_stat : string -> Unix.stats option +(** safe version of Pervasives.prerr_endline + (avoid exception in win32 without console) *) +val safe_prerr_endline : string -> unit +(** debug printing *) val prerr_endline : string -> unit -val prerr_string : string -> unit + val print_id : 'a -> unit val revert_timer : GMain.Timeout.id option ref |