aboutsummaryrefslogtreecommitdiff
path: root/lib/errors.ml
diff options
context:
space:
mode:
authorEnrico Tassi2015-02-23 17:14:05 +0100
committerEnrico Tassi2015-02-23 17:14:05 +0100
commite87ca456fb4cbe54f09e13f1e20d504d2699ac2b (patch)
tree41b358ee2deb7c614e39f7db27368f9626c19778 /lib/errors.ml
parent28781f3fd6ae6e7f281f906721e8a028679ca089 (diff)
parentdf2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (diff)
Merge branch 'v8.5' into trunk
Diffstat (limited to 'lib/errors.ml')
-rw-r--r--lib/errors.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/errors.ml b/lib/errors.ml
index ab331d6a4d..a4ec357ee4 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -108,7 +108,7 @@ let _ = register_handler begin function
| _ -> raise Unhandled
end
-(** Critical exceptions shouldn't be catched and ignored by mistake
+(** Critical exceptions should not be caught and ignored by mistake
by inner functions during a [vernacinterp]. They should be handled
only at the very end of interp, to be displayed to the user. *)