#!/bin/bash

set -e

DIR=`dirname $0`

source ${DIR}/common.sh

T="${DIR}/build.sh"
start_timer "$T"
${DIR}/build.sh
end_timer "$T"

T="make site"
start_timer "$T"
(cd website && make travis-site)
end_timer "$T"

T="${DIR}/test.sh"
start_timer "$T"
${DIR}/test.sh
end_timer "$T"

print_timer_summary