Comando time no zsh (shell Linux)

Publicado por felipe gallois em 06/10/2008

[ Hits: 7.229 ]

 


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

Adicionando múltiplos usuários no Linux com VIM

Auctex: Tabela de atalhos

Iniciar o KTorrent via SSH (Linux remoto)

Leitura recomendada

Como criar um atalho de navegação anônima no Chrome ou no Chromium

Flash Player no cliente nativo do Steam - Instalação no Ubuntu 12.04 64 bits

Fuce no que você não sabe, um dia você aprenderá

Guia Foca Linux em sua Área de Trabalho

FlareGet, acelerador de downloads no Ubuntu

  

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