diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 8269582d..1fb30e4d 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -29,7 +29,7 @@ val find_tag_limits : GText.tag -> GText.iter -> GText.iter * GText.iter val find_tag_start : GText.tag -> GText.iter -> GText.iter val find_tag_stop : GText.tag -> GText.iter -> GText.iter -val select_file_for_open : title:string -> unit -> string option +val select_file_for_open : title:string -> ?filename:string -> unit -> string option val select_file_for_save : title:string -> ?filename:string -> unit -> string option val try_convert : string -> string @@ -71,7 +71,7 @@ val default_logger : Pp.message_level -> string -> unit (** {6 I/O operations} *) -(** A customized [stat] function. Exceptions are catched. *) +(** A customized [stat] function. Exceptions are caught. *) type stats = MTime of float | NoSuchFile | OtherError val stat : string -> stats |