diff options
| -rw-r--r-- | utils/warnings.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/utils/warnings.mli b/utils/warnings.mli index 9a5d9abd6..dd3a5ecf5 100644 --- a/utils/warnings.mli +++ b/utils/warnings.mli @@ -42,14 +42,14 @@ type t = | Unused_var_strict of string (* 27 *) | Wildcard_arg_to_constant_constr (* 28 *) | Eol_in_string (* 29 *) - | Duplicate_definitions of string * string * string * string (*30 *) + | Duplicate_definitions of string * string * string * string (* 30 *) | Multiple_definition of string * string * string (* 31 *) | Unused_value_declaration of string (* 32 *) | Unused_open of string (* 33 *) | Unused_type_declaration of string (* 34 *) | Unused_for_index of string (* 35 *) | Unused_ancestor of string (* 36 *) - | Unused_constructor of string * bool * bool (* 37 *) + | Unused_constructor of string * bool * bool (* 37 *) | Unused_exception of string * bool (* 38 *) | Unused_rec_flag (* 39 *) | Name_out_of_scope of string list * bool (* 40 *) |