aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Diagnostics.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-02-09 09:53:12 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-02-09 09:53:12 +0100
commit857e746959f1eb9d0158073114d5ae0aa1c2fc1f (patch)
tree63e38025de7e855da2e3aec1a5220de03313dd1d /cparser/Diagnostics.mli
parentd8da506981905752f84165f622fdf0ee26011744 (diff)
downloadcompcert-kvx-857e746959f1eb9d0158073114d5ae0aa1c2fc1f.tar.gz
compcert-kvx-857e746959f1eb9d0158073114d5ae0aa1c2fc1f.zip
Added error summary in case of fatal error.
Diffstat (limited to 'cparser/Diagnostics.mli')
-rw-r--r--cparser/Diagnostics.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index 54395136..82edd9fa 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -84,3 +84,6 @@ val no_loc : string * int
val file_loc : string -> string * int
(** [file_loc f] generates a location for file [f] *)
+
+val error_summary : unit -> unit
+(** Print a summary containing the numbers of errors encountered *)