#!/bin/bash
set -e
SCRIPT_DIR=$(cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd)
cd "$SCRIPT_DIR"
cat time.txt | \
tr '\n' '#' | \
sed 's/real//g;s/user//g;s/sys//g;s/ */,/g;s/,#,/,/g;s/,#/#/g' | \
tr '#' '\n' | \
awk 'BEGIN { print "ltl,n,length,r,real,user,sys" } { print $0 }' > time.csv
