equal
deleted
inserted
replaced
13 log_cmd "$@" |
13 log_cmd "$@" |
14 |
14 |
15 "$@" || die "Failed" |
15 "$@" || die "Failed" |
16 } |
16 } |
17 |
17 |
|
18 ## Execute command, prefixing its output on stdout with given indent prefix. |
|
19 # |
|
20 # indent " " $cmd... |
|
21 # |
|
22 # Output is kept on stdout, exit status is that of the given command. |
|
23 # Also logs the executed command at log_cmd level.. |
18 function indent () { |
24 function indent () { |
19 local indent=$1; shift |
25 local indent=$1; shift |
20 |
26 |
21 log_cmd "$@" |
27 log_cmd "$@" |
22 |
28 |