Using the built-in "time" command in bash rather than the external command

Question

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 enable and/or 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:

Make bash use external `time` command rather than shell built-in

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).

see here on how to force bash to use builtins, see answer2 by Petr Utzl: builtin time should do the trick. — FelixJN, Aug 14 '15 at 13:34
@Fiximan, time is not a builtin in bash, it's a reserved word of the language so you can time pipelines (like time foo | bar) or compound commands (like time for i in...;done) — Stéphane Chazelas, Aug 14 '15 at 15:09

score 14 · Accepted Answer · edited Aug 14 '15 at 14:06

By default, watch runs your command with /bin/sh -c '...' so the output you see is how /bin/sh interprets the time command. Your /bin/sh apparently doesn't have a builtin time.

To run the command with a different shell, use the -x option to get rid of the default, then add your own explicit invocation of the shell whose builtin you want.

watch -x bash -c 'time ls'
watch -x zsh -c 'time ls'

No matter how you run watch, the command you're watching is not a child of the shell that ran the watch command, so that shell's settings aren't directly relevant.

Using the built-in "time" command in bash rather than the external command

1 Answers1

Linked