1 2 3 4 5 6 7 8
# utilities used in CI pipelines to avoid duplication. echo_run () { # echo's a command before running it, which helps understanding logs echo "" echo "$@" "$@" }