Usando o comando “time” embutido no bash ao invés do comando externo

Question

Trabalhando com o comando time , me deparei com uma situação em que deveria use o comando time embutido em vez do comando de tempo GNU externo /usr/bin/time . Então, como posso fazer isso? Eu vi em algum lugar que usar enable e / ou command ajudaria, mas eles não ajudaram.

Este é um caso de uso:

watch "time ls"

que usa o comando /usr/bin/time externo, que eu não quero! Isso acontece quando time invoca a função bash interna quando eu executo time ls em um terminal, assim:

$ time ls

Por favor, note que o pedido oposto exato foi respondido aqui:

• Faça o uso de bash externo ' comando time 'em vez de shell embutido

Há muita diferença com dois comandos. O time interno é mais preciso (o que eu quero), mas o comando externo tem mais opções (que eu não preciso).

    

Answer 1

Por padrão, watch executa seu comando com /bin/sh -c '...' , então a saída que você vê é como /bin/sh interpreta o comando time . Seu /bin/sh aparentemente não possui um time .

Para executar o comando com um shell diferente, use a opção -x para se livrar do padrão e, em seguida, adicione sua própria invocação explícita do shell cujo builtin você deseja.

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

Não importa como você executa watch , o comando que você está assistindo não é filho do shell que executou o comando watch , portanto as configurações do shell não são diretamente relevantes.