diff options
| author | Hugo Herbelin | 2017-09-11 09:27:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-13 18:59:32 +0200 |
| commit | 240c8bffaa788669cf3135c95d067cc7b11b5da1 (patch) | |
| tree | 2a4cf2e33bc08e760fb2fe4b93e7a0f6b6c706ac /lib/unicode.mli | |
| parent | e88dfedd99a84e9e375f3583be6fd1de3de36c72 (diff) | |
Adding a function to escape strings with non-utf8 characters.
Diffstat (limited to 'lib/unicode.mli')
| -rw-r--r-- | lib/unicode.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/unicode.mli b/lib/unicode.mli index c7d7424801..b8e7c33ad4 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -40,3 +40,6 @@ val utf8_length : string -> int (** Variant of {!String.sub} for UTF-8 strings. *) val utf8_sub : string -> int -> int -> string + +(** Return a "%XX"-escaped string if it contains non UTF-8 characters. *) +val escaped_if_non_utf8 : string -> string |