Process handling
#
p_name
| : string | ; | (* | Command name | *) |
#
p_args
| : string list | ; | (* | Command args | *) |
#
p_pid
| : int | ; | (* | Process PID | *) |
#
p_cwd
| : string | ; | (* | Process initial working directory | *) |
#
p_time
| : float | ; | (* | Process start time | *) |
#
p_stdout
| : string option | ; | (* | stdout dump file | *) |
#
p_stderr
| : string option | ; | (* | stderr dump file | *) |
#
p_env
| : string option | ; | (* | dump environment variables | *) |
#
p_info
| : string option | ; | (* | dump process info | *) |
#
p_metadata
| : (string * string) list | ; | (* | Metadata associated to the process | *) |
The type for processes
create cmd args
create a new process to execute the command
cmd
with arguments args
. If stdout_file
or stderr_file
are
set, the channels are redirected to the corresponding files. The
outputs are discarded is verbose
is set to false. The current
environment can also be overriden if env
is set. The environment
which is used to run the process is recorded into env_file
(if
set).
#
r_code
| : int | ; | (* | Process exit code | *) |
#
r_duration
| : float | ; | (* | Process duration | *) |
#
r_info
| : (string * string) list | ; | (* | Process info | *) |
#
r_stdout
| : string list | ; | (* | Content of stdout dump file | *) |
#
r_stderr
| : string list | ; | (* | Content of stderr dump file | *) |
#
r_cleanup
| : string list | ; | (* | List of files to clean-up | *) |
Process results
run ~name cmd args
synchronously call the command cmd
with
arguments args
. It waits until the process is finished. The file
name.info
, name.env
, name.out
and name.err
and are
created, and contains the process main description, the environment
variables, the standard output and the standard error.
Pretty printing of process.