diff options
Diffstat (limited to 'src/reporting.mli')
| -rw-r--r-- | src/reporting.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/reporting.mli b/src/reporting.mli index e0744c66..54875398 100644 --- a/src/reporting.mli +++ b/src/reporting.mli @@ -116,6 +116,9 @@ val print_error : error -> unit location, the second after. *) val warn : string -> Parse_ast.l -> string -> unit +(** Print a simple one-line warning without a location. *) +val simple_warn: string -> unit + (** Will suppress all warnings for a given file. Used by $suppress_warnings directive in process_file.ml *) val suppress_warnings_for_file : string -> unit |