Comando time no zsh (shell Linux)

Publicado por felipe gallois em 06/10/2008

[ Hits: 7.184 ]

 


Comando time no zsh (shell Linux)



O zsh tem uma mania feia de formatar o time bem diferente do bash (não sei se é feia mesmo ou eu que não curto xD).

time who
...
who 0.00s user 0.00s system 24% cpu 0.016 total

Beleza, isso é fácil de resolver:

time -p who
zsh: command not found: -p
zsh: exit 127 -p who
-p who 0.00s user 0.00s system 0% cpu 0.001 total

ops Oo ...

time --help
zsh: command not found: --help
zsh: exit 127 --help
--help 0.00s user 0.00s system 0% cpu 0.017 total

oops[2] oO ...

which time
time: shell reserved word

Hmmm ...

type -a time
time is a reserved word
time is /usr/bin/time

Agora faz sentido, estamos usando uma palavra reservada do shell, não o time que queremos!

Como resolver

Moleza!

alias time="/usr/bin/time -p"

Pronto. =]

Mas digitar isso toda vez que iniciar o shell é chato, portanto adicione no seu arquivo .zshrc:

alias time="/usr/bin/time -p"

Resolvido o problema. =]

type -a time
time is an alias for /usr/bin/time -p
time is a reserved word
time is /usr/bin/time

Referência

meu blog xD
zsh + time, sem opções - gallois' blag

Abraços!

Outras dicas deste autor

Iniciar o KTorrent via SSH (Linux remoto)

Auctex: Tabela de atalhos

Adicionando múltiplos usuários no Linux com VIM

Leitura recomendada

Montando um servidor de remote desktop com NX Server

GTA San Andreas online

Etapas do desenvolvimento do kernel

Terminator - O multi-terminal do Linux

VirtualBox 4.3 no Debian 8 (Jessie) 64bits

  

Comentários
[1] Comentário enviado por SMarcell em 24/02/2009 - 02:04h

Outra maneira de contornar isso, seria alterando a variável built-in 'TIMEFMT'.



Contribuir com comentário




Patrocínio

Site hospedado pelo provedor RedeHost.
Linux banner

Destaques

Artigos

Dicas

Tópicos

Top 10 do mês

Scripts