commande time et redirection

Bonjour,

Je cherche a mesurer le temps d'execution d'une commande.
J'utilise la commande shell builtin time, je ne veux récupérer que le
résultat de la commande time:
$ time ./mon_programme > /dev/null
real 50m6.306s
user 49m59.307s
sys 0m1.696s

OK. Mais comment récuperer ces valeurs dans un fichier?

le programme /usr/bin/time dispose des argument -ao pour mettre les
valeurs dans le fichier, mais comment faire avec le shell builtin time?
[...]

$ time ./mon_programme > /dev/null
real 50m6.306s
user 49m59.307s
sys 0m1.696s

OK. Mais comment récuperer ces valeurs dans un fichier?

"time" n'est pas un builtin, c'est un keyword.

{ { time ./mon_programme 2>&3 3>&-; } 2> time.out ; } 3>&2

OK. Mais comment récuperer ces valeurs dans un fichier?

"time" n'est pas un builtin, c'est un keyword.

{ { time ./mon_programme 2>&3 3>&-; } 2> time.out ; } 3>&2

Je ne connais pas « &- ». Qu'est-ce que c'est ? Cela fonctionne quel que
soit le shell, y compris le dinosauresque bourne shell ? Et dans ksh ?

3>&- ferme le descripteur 3 (ici pour ./mon_programme qui n'en a
pas besoin).

La syntaxe ci-dessous est Bourne et POSIX donc marchera avec
tous les shells Bourne-like.

(le Bourne shell n'a pas de keyword "time", note, POSIX
l'autorise mais ne requiert pas qu'il soit un keyword).