Comando time no zsh (shell Linux)

Publicado por felipe gallois em 06/10/2008

[ Hits: 6.949 ]

 


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)

Adicionando múltiplos usuários no Linux com VIM

Auctex: Tabela de atalhos

Leitura recomendada

Zentyal 2.2 disponível para download

Wayland, um servidor gráfico não-X muito interessante

Configurando servidor DHCP no Debian 8

Você já leu a GPL?

Configurando dois monitores em uma única placa de vídeo no Ubuntu 9.10

  

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