#!/bin/sh

header() {
    echo ""
    echo "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%"
    echo $1
    echo "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%"
    echo ""
}

runcmd() {
    echo " => $1"
    time sh -c "$1"
    ret=$?
    return $ret
}

die () { echo >&2 "ERROR: $*" ; exit 1 ; }