15

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

Improve this question
3
  • watch 'bash -c "builtin time ls"' perhaps? Commented Aug 14, 2015 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. Commented Aug 14, 2015 at 13:34
  • 3
    @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) Commented Aug 14, 2015 at 15:09

1 Answer 1

Reset to default
15

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.

Improve this answer

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.