diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-02-09 09:53:12 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-02-09 09:53:12 +0100 |
commit | 857e746959f1eb9d0158073114d5ae0aa1c2fc1f (patch) | |
tree | 63e38025de7e855da2e3aec1a5220de03313dd1d /cparser/Diagnostics.mli | |
parent | d8da506981905752f84165f622fdf0ee26011744 (diff) | |
download | compcert-857e746959f1eb9d0158073114d5ae0aa1c2fc1f.tar.gz compcert-857e746959f1eb9d0158073114d5ae0aa1c2fc1f.zip |
Added error summary in case of fatal error.
Diffstat (limited to 'cparser/Diagnostics.mli')
-rw-r--r-- | cparser/Diagnostics.mli | 3 |
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 *) |