#!/bin/bash
# Adds timestamps to all lines on stdin, and prints them to stdout as well as a log file.
# The version printed to stdout has the specified prefix on each line.

set -e
set -o pipefail

PREFIX="$1"
LOGFILE="$2"
shift
shift

function cleanup()
{
  local pids=`jobs -p`
  set +e
  if [[ "$pids" != "" ]]; then
    kill $pids >/dev/null 2>/dev/null
  fi
  if [[ "$TEMPDIR" != "" ]]; then
    rm -rf "$TEMPDIR"
  fi
}

function add_timestamps()
{
  gawk '{ print strftime("%Y-%m-%d %H:%M:%S --"), $0; fflush(); }'
}

function forward_multiple()
{
  while read LINE; do
    echo "$LINE" >&3
    echo "${PREFIX}: ${LINE}"
  done
}

trap cleanup EXIT
exec 3>>"$LOGFILE"
"$@" 2>&1 | add_timestamps | forward_multiple
