quote_command cmd args returns a quoted command line, suitable for use as an argument to Sys.command, Unix.system, and the Unix.open_process functions.
The string cmd is the command to call. The list args is the list of arguments to pass to this command. It can be empty.
The optional arguments ?stdin and ?stdout and ?stderr are file names used to redirect the standard input, the standard output, or the standard error of the command. If ~stdin:f is given, a redirection < f is performed and the standard input of the command reads from file f. If ~stdout:f is given, a redirection > f is performed and the standard output of the command is written to file f. If ~stderr:f is given, a redirection 2> f is performed and the standard error of the command is written to file f. If both ~stdout:f and ~stderr:f are given, with the exact same file name f, a 2>&1 redirection is performed so that the standard output and the standard error of the command are interleaved and redirected to the same file f.
Under Unix and Cygwin, the command, the arguments, and the redirections if any are quoted using Filename.quote, then concatenated. Under Win32, additional quoting is performed as required by the cmd.exe shell that is called by Sys.command.