diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-29 12:35:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-23 19:22:06 +0100 |
| commit | 23f49985296a3594c2cf37fa08e0b3e882d5c9e4 (patch) | |
| tree | f4c49227a8304c0d263cfe3d6a9e0c7fb6952bfd /lib | |
| parent | 6b88c2d18e6aba570c73aa22299abe1fa3f19039 (diff) | |
Add a function to surround filenames containing a space with quotes.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cUnix.ml | 5 | ||||
| -rw-r--r-- | lib/cUnix.mli | 3 |
2 files changed, 8 insertions, 0 deletions
diff --git a/lib/cUnix.ml b/lib/cUnix.ml index 867f86a74..34fb660db 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 diff --git a/lib/cUnix.mli b/lib/cUnix.mli index a39481404..f79f34016 100644 --- a/lib/cUnix.mli +++ b/lib/cUnix.mli @@ -14,6 +14,9 @@ type load_path = physical_path list val physical_path_of_string : string -> physical_path val string_of_physical_path : physical_path -> string +(** Escape what has to be escaped (e.g. surround with quotes if with spaces) *) +val escaped_string_of_physical_path : physical_path -> string + val canonical_path_name : string -> string (** remove all initial "./" in a path *) |