diff options
Diffstat (limited to 'utils/warnings.mli')
| -rw-r--r-- | utils/warnings.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/utils/warnings.mli b/utils/warnings.mli index c9ab96cc3a..1d41612540 100644 --- a/utils/warnings.mli +++ b/utils/warnings.mli @@ -18,7 +18,7 @@ type t = | Deprecated of string (* 3 *) | Fragile_match of string (* 4 *) | Partial_application (* 5 *) - | Labels_omitted (* 6 *) + | Labels_omitted of string list (* 6 *) | Method_override of string list (* 7 *) | Partial_match of string (* 8 *) | Non_closed_record_pattern of string (* 9 *) |