#!/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