Working with the
time command, I came across a situation where I should
use the built-in
time rather than the external GNU time command
/usr/bin/time. So, how can I do this? I saw somewhere that using
command would help, but they didn't.
This is a use case:
watch "time ls"
which uses the external
/usr/bin/time command, which I don't want! This happens when
time invokes the internal bash function when I run
time ls on a terminal, like this:
$ time ls
Please note that the exact opposite request has been answered here:
There is a lot of difference with two commands. The internal
time is more precise (which I want), but the external command has more options (which I do not need).