Comment by marbu

A minor nitpick: the author most likely doesn't use time(1), which usually is https://www.gnu.org/software/time/), but internal shell command time. See:

``` $ type -a time time is a shell keyword time is /usr/bin/time time is /bin/time ```