time
é muitas coisas. Existe o /usr/bin/time
programa GNU externo. Há a palavra-chave bash time
.
$ type -a time
time is a shell keyword
time is /usr/bin/time
Quando você executa time …
em um shell interativo, normalmente usa o bash e, portanto, a palavra-chave time
entra em vigor.
Quando você executa time …
em um script usando /bin/sh
, o shell usado ( dash
)
não tem time
como palavra-chave, e o comando% time
externo é chamado.
Para obter o resultado desejado, ligue para o time
externo. comando com a opção -p
:
-p, --portability
Use the following format string, for conformance with POSIX
standard 1003.2:
real %e
user %U
sys %S
O comando externo também é mais amigável. Como não é uma palavra-chave, você não precisa fazer o truque wrap-in { … }
-for-redirecionamento para obter a saída em um arquivo. Há uma opção para isso:
-o FILE, --output=FILE
Write the resource use statistics to FILE instead of to the
standard error stream. By default, this overwrites the file,
destroying the file's previous contents. This option is useful
for collecting information on interactive programs and programs
that produce output on the standard error stream.
A saída também é muito mais personalizável, facilitando o processamento posterior. Com time
do bash, as opções fornecidas em TIMEFORMAT
são muito limitadas.