12

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:

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

  • watch 'bash -c "builtin time ls"' perhaps? – glenn jackman Aug 14 '15 at 13:23
  • 1
    see here on how to force bash to use builtins, see answer2 by Petr Utzl: builtin time should do the trick. – Fiximan Aug 14 '15 at 13:34
  • 2
    @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
12

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.