diff options
| author | Maxime Dénès | 2017-11-27 16:45:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-27 16:45:03 +0100 |
| commit | 86cada15ad12e31b1f9fe6f0b7026860f45671b4 (patch) | |
| tree | 00815df07b0e6d0e8367b98b2db3a5863129bc69 /lib/cUnix.ml | |
| parent | 4774a3129f4175b0b97d538a1c61eb084332fd85 (diff) | |
| parent | f36ea3ffb4ef01572db437392174f10650bee67b (diff) | |
Merge PR #6041: Protecting the printing of filenames with space
Diffstat (limited to 'lib/cUnix.ml')
| -rw-r--r-- | lib/cUnix.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/cUnix.ml b/lib/cUnix.ml index 867f86a746..34fb660db4 100644 --- a/lib/cUnix.ml +++ b/lib/cUnix.ml @@ -14,6 +14,11 @@ type load_path = physical_path list let physical_path_of_string s = s let string_of_physical_path p = p +let escaped_string_of_physical_path p = + (* We assume a reasonable-enough path (typically utf8) and prevents + the presence of space; other escapings might be useful... *) + if String.contains p ' ' then "\"" ^ p ^ "\"" else p + let path_to_list p = let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in Str.split sep p |