summaryrefslogtreecommitdiff
path: root/Changes
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2019-06-25 14:21:58 +0200
committerDamien Doligez <damien.doligez@inria.fr>2019-06-25 14:21:58 +0200
commita8daa89500f2aee6d73b6915928f9f65f0a8dff3 (patch)
tree746c3c14d92ea2314a4992884c738cc689808cba /Changes
parentd8b6a1713b50132fc96b6cda40c8aad4ec4f8008 (diff)
downloadocaml-a8daa89500f2aee6d73b6915928f9f65f0a8dff3.tar.gz
Add Filename.quote_command function (#1492)
MPR#7672: add a Filename.quote_command function This function takes care of quoting the command and its arguments so that they are correctly parsed by the system shell (/bin/sh for Unix, cmd.exe for Win32). Redirections for std input (< file) and std output (> file) and std error (2> file) can also be specified as optional arguments. A 2>&1 redirection is used if stdout and stderr are redirected to the same file. The result is a string that can be passed directly to Sys.command or to the Unix functions that expect shell command lines.
Diffstat (limited to 'Changes')
-rw-r--r--Changes4
1 files changed, 4 insertions, 0 deletions
diff --git a/Changes b/Changes
index bc485a5daa..c3686b9272 100644
--- a/Changes
+++ b/Changes
@@ -63,6 +63,10 @@ Working version
(Jacques-Henri Jourdan, review by Stephen Dolan, Gabriel Scherer and
Damien Doligez)
+- #7672, #1492: Add `Filename.quote_command` to produce properly-quoted
+ commands for execution by Sys.command.
+ (Xavier Leroy, review by David Allsopp and Damien Doligez)
+
### Other libraries:
- #1939, #2023: Implement Unix.truncate and Unix.ftruncate on Windows.