On: Pipes and Filters

[pdknsk]

> I’m calling /usr/bin/time here to avoid using my shell’s built-in time command [...].

I prefer to use command in this scenario.

$ command time