diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 23b31e4ae..977aa0c14 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -30,9 +30,6 @@ 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 |