aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/cerrors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/cerrors.ml')
-rw-r--r--toplevel/cerrors.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index f34621216..4250040ec 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -45,6 +45,8 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (str "Out of memory.")
| Stack_overflow ->
hov 0 (str "Stack overflow.")
+ | Timeout ->
+ hov 0 (str "Timeout!")
| Anomaly (s,pps) ->
hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
| Match_failure(filename,pos1,pos2) ->