#!/bin/bash
#
# bench/time: runs a program, discards stdout and print name and runtime
#
# Copyright (C) 2021 Rudy Matela
# Distributed under the 3-Clause BSD licence (see the file LICENSE).

printf "%-14s  " "$*"
/usr/bin/time -f%e "$@" >/dev/null