diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index b317c849cc..ccd807a90a 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -290,6 +290,7 @@ let check_ident s = | _ -> error (s^": an identifier should start with a letter") with | End_of_input -> error "The empty string is not an identifier" + | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence") | Invalid_argument _ -> error (s^": invalid utf8 sequence") (* Lists *) |