aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-11 16:22:51 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-13 19:00:42 +0200
commite9cd8ef01fe5b9ffc3e85984d0f9bc410a56f8ea (patch)
tree83c8aecf396757eec746503345e4bf62b8397e47 /lib
parent2938fceb50b71d4784d6d718021c505c00196f50 (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 'lib')
-rw-r--r--lib/system.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 12eacf2ea..0b64b237d 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -52,7 +52,7 @@ let dirmap = ref StrMap.empty
let make_dir_table dir =
let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
- Array.fold_left filter_dotfiles StrSet.empty (readdir dir)
+ Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
let exists_in_dir_respecting_case dir bf =
let cache_dir dir =