O comando "time" do Unix com pipeline imprime sem relatório de tempo

Question

Dos dois aliases do C-shell abaixo, apenas o primeiro imprime o relatório do tempo decorrido do comando time . Como posso obter o alias com o pipeline para também imprimir o relatório de tempo?

alias make1 'time make'

alias make2 'time make |& tee make.log'

    

Answer 1

O comando time embutido no shell C (csh ou tcsh) não funciona com pipelines. Para evitar essa limitação, use a página de manual independente tempo , que geralmente é encontrado em / usr / bin / time (se não estiver, tente whereis time para localizá-lo).

Altere time em sua linha de comando para /usr/bin/time (ou /usr/bin/time -p ) ou qualquer que seja o caminho para o programa de horário, e isso deve funcionar.

Por que não funcionou:

O shell C (como alguns outros shells) tem um comando time (veja o página de manual do builtin ), que é usada preferencialmente ao programa de horário não integrado (independente):

% which time
time: shell built-in command.
% 

e a página man do csh (na verdade tcsh na minha sistema) afirma:

time [command]
   Executes command (which must be a simple command, not an alias,
   a pipeline, a command list or a parenthesized command list) ...

O comando / usr / bin / time não tem essa limitação, e nem os comandos in time da maioria das outras shells, por exemplo, bash ou zsh.

    

Answer 2

Você quis usar um tubo lá? O que você está fazendo essencialmente é canalizar o resultado do segundo comando time para tee . É por isso que o resultado não está sendo impresso - provavelmente está sendo escrito em make.log.