aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-02-23 11:26:51 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-02-23 13:37:52 +0100
commitdf2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (patch)
treec11084a17eec2bc25bdcbba715aa1ba50b108272 /ide
parent705bf896bfc552e95403d097fe9b8031c598d88b (diff)
Fix some typos in comments.
Diffstat (limited to 'ide')
-rw-r--r--ide/ideutils.ml2
-rw-r--r--ide/ideutils.mli2
2 files changed, 2 insertions, 2 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 473b8dc82..973ff0b77 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -285,7 +285,7 @@ let default_logger level message =
(** {6 File operations} *)
-(** A customized [stat] function. Exceptions are catched. *)
+(** A customized [stat] function. Exceptions are caught. *)
type stats = MTime of float | NoSuchFile | OtherError
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 8269582df..c2b51dd39 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -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