summaryrefslogtreecommitdiff
path: root/checker/checker.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-19 13:13:14 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-19 13:13:14 +0100
commita0a94c1340a63cdb824507b973393882666ba52a (patch)
tree73aa4eb32cbd176379bc91b21c184e2a6882bfe3 /checker/checker.ml
parentcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff)
Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg
Diffstat (limited to 'checker/checker.ml')
-rw-r--r--checker/checker.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 3d928933..70e2eb97 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -256,7 +256,7 @@ let rec explain_exn = function
| Not_found ->
hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
| Failure s ->
- hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report ())
+ hov 0 (str "Failure: " ++ str s ++ report ())
| Invalid_argument s ->
hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
| Sys.Break ->
@@ -385,4 +385,4 @@ let run () =
flush_all();
exit 1)
-let start () = init(); run(); exit 0
+let start () = init(); run(); Check_stat.stats(); exit 0