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.mli | |
| parent | 4774a3129f4175b0b97d538a1c61eb084332fd85 (diff) | |
| parent | f36ea3ffb4ef01572db437392174f10650bee67b (diff) | |
Merge PR #6041: Protecting the printing of filenames with space
Diffstat (limited to 'lib/cUnix.mli')
| -rw-r--r-- | lib/cUnix.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/cUnix.mli b/lib/cUnix.mli index a394814041..d08dc4c403 100644 --- a/lib/cUnix.mli +++ b/lib/cUnix.mli @@ -14,9 +14,12 @@ 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 *) +(** Remove all initial "./" in a path *) val remove_path_dot : string -> string (** If a path [p] starts with the current directory $PWD then @@ -61,6 +64,6 @@ val sys_command : string -> string list -> Unix.process_status val waitpid_non_intr : int -> Unix.process_status -(** checks if two file names refer to the same (existing) file *) +(** Check if two file names refer to the same (existing) file *) val same_file : string -> string -> bool |