diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-11 16:22:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-13 19:00:42 +0200 |
| commit | e9cd8ef01fe5b9ffc3e85984d0f9bc410a56f8ea (patch) | |
| tree | 83c8aecf396757eec746503345e4bf62b8397e47 /vernac/mltop.ml | |
| parent | 2938fceb50b71d4784d6d718021c505c00196f50 (diff) | |
A possible fix for BZ#5715 (escape non-utf8 win32 file names).
On Win32, Sys.readdir translates the file names to the charset of the
local "code page", which may be not compatible with utf8.
Warnings referring to these names can be generated. These warnings may
be sent to CoqIDE. To ensure a utf8 compliant communication, we escape
non-utf8 file names under win32.
In the CoqIDE/Coq communication, Glib.IO.read_chars expects an
utf8-encoding and raises otherwise a Glib.Error "Invalid byte sequence in
conversion input".
This fixes bug #5715 (Hangul characters not recognized in file names)
but this does not solve the case of an operating system mounting a
file system with a different coding convention than the default one,
i.e. unicode using "Normalization Form Canonical Decomposition" in
UTF-8 for HFS+ on MacOS X, no encoding for ext3/ext4 on Linux,
(non-normalized?) UTF-16 for NTFS on Windows.
Diffstat (limited to 'vernac/mltop.ml')
| -rw-r--r-- | vernac/mltop.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/mltop.ml b/vernac/mltop.ml index e8a0ba3dd..8ec85688c 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -175,6 +175,7 @@ let warn_cannot_use_directory = let convert_string d = try Names.Id.of_string d with UserError _ -> + let d = Unicode.escaped_if_non_utf8 d in warn_cannot_use_directory d; raise Exit |