diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 10:25:25 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 10:25:25 +0000 |
commit | 93d89c2b5e8497365be152fb53cb6cd4c5764d34 (patch) | |
tree | 0de8d05bbd0eeaeb5e4b85395f8dd576984b6a9e /cil/bin/teetwo | |
parent | 891377ce1962cdb31357d6580d6546ec22df2b4f (diff) | |
download | compcert-93d89c2b5e8497365be152fb53cb6cd4c5764d34.tar.gz compcert-93d89c2b5e8497365be152fb53cb6cd4c5764d34.zip |
Getting rid of CIL
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cil/bin/teetwo')
-rwxr-xr-x | cil/bin/teetwo | 36 |
1 files changed, 0 insertions, 36 deletions
diff --git a/cil/bin/teetwo b/cil/bin/teetwo deleted file mode 100755 index 2aa68fa5..00000000 --- a/cil/bin/teetwo +++ /dev/null @@ -1,36 +0,0 @@ -#!/bin/bash -# run a command, sending stdout to one file and stderr to another, -# but also sending both to this process' stdout/stderr, respectively - -if [ "$3" = "" ]; then - echo "usage: $0 stdout-file stderr-file cmd [args..]" - exit 0 -fi - -stdoutFile="$1" -stderrFile="$2" -command="$3" -shift -shift -shift - -result=0 -handler() { - # this signal means the underlying command exit erroneously, - # though we don't know the code - echo "The command failed!" - result=2 -} -trap handler SIGUSR1 - -# dup my stdout/err on fd 3,4 -exec 3>&1 -exec 4>&2 - - -# run the command with tees to duplicate the data -mypid=$$ -# echo "mypid = $mypid, command=$command, args=$@, stdout=$stdoutFile, stderr=$stderrFile" -(("$command" "$@" || kill -s USR1 $mypid) | tee "$stdoutFile" >&3) 2>&1 | tee "$stderrFile" >&4 - -exit $result |