diff options
Diffstat (limited to 'dev/ci/ci-pipe-tee.sh')
-rwxr-xr-x | dev/ci/ci-pipe-tee.sh | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/dev/ci/ci-pipe-tee.sh b/dev/ci/ci-pipe-tee.sh deleted file mode 100755 index 7b1ccddf2..000000000 --- a/dev/ci/ci-pipe-tee.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -# Use this script to preserve the exit code of $1 when piping it to -# `tee $2`. We have a separate script, because this only works in -# bash, which we don't require project-wide. - -"$1" 2>&1 | tee "$2" -exit ${PIPESTATUS[0]} |