Getting rid of CIL

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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