diff options
author | Chimrod <> | 2024-12-28 09:57:05 +0100 |
---|---|---|
committer | Chimrod <> | 2024-12-28 09:57:15 +0100 |
commit | 289dc576624d4233116806e566bb791fee1de178 (patch) | |
tree | 775b292c5f66c3cc6725511c5341e9ee7fd5790a /test/dup_cases.ml | |
parent | 9b831d2a2401c771cf43a37b27c8909d6b9c9ba8 (diff) |
Changed the error message for duplicated cases from Error to Warning
Diffstat (limited to 'test/dup_cases.ml')
-rw-r--r-- | test/dup_cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/dup_cases.ml b/test/dup_cases.ml index 8d4274e..8b9f846 100644 --- a/test/dup_cases.ml +++ b/test/dup_cases.ml @@ -59,7 +59,7 @@ end |} [ { - level = Error; + level = Warn; loc = _position; message = "This case is duplicated line(s) 5"; }; @@ -79,7 +79,7 @@ end |} [ { - level = Error; + level = Warn; loc = _position; message = "This case is duplicated line(s) 6"; }; |