Vanuxem Grégory a écrit :
Le vendredi 04 août 2006 à 13:06 +0200, Guy Roussin a écrit :
Peut etre que time est une commande interne au shell utilisé
ou qu'elle est aliasée ?
essayer :
\time --version
Oui, si tu utilises bash, 'help time' dans un terminal devrait t'en dire
plus (ou 'alias time').
J'avais vérifié pour les alias.
help time ne m'apprend rien (ça raconte ce que ça fait mais pas qui le fait,
bash ou binaire indépendant du shell), en revanche dans le man bash on
trouve que time est un mot réservé.
La commande type, que j'avais oubliée est bien utile dans ce cas là :
$type time
time is a shell keyword
$type echo
echo is a shell builtin
$type ls
ls is aliased to `ls $LS_OPTIONS'
$type cat
cat is /bin/cat
Sinon, effectivement
\time
fonctionne comme
/usr/bin/time
Si je comprend bien, l'anti-slash indique au shell de faire passer la commande
externe avant la commande interne. On en apprend tous les jours... (et
on devrait relire le man bash de temps en temps, mais il est vraiment long ;-) )
Daniel
PS: désolé pour le post en double, j'avais pas reçu le 1er et j'ai changé
d'adresse d'expéditeur pensant m'être planté la 1re fois).
PS2: désolé pour les mails en PV, j'ai l'habitude du reply sans regarder sur
les ml.
Greg
