#!/bin/bash

TIME=$(which time)

echo "runtests"
${TIME} -f 'Execution time: %e s' bash -c "./runtests -v"
echo "runtestspp"
${TIME} -f 'Execution time: %e s' bash -c "./runtests_cxx -v"
echo