This is a bug in the bash built-in version of time, not the "real" time command (/usr/bin/time).
/usr/bin/time does not exhibit this behaviour. -- Gilbert Laycock email: [EMAIL PROTECTED] Maths and Computer Science, http://www.mcs.le.ac.uk/~glaycock University of Leicester phone: (+44) 116 252 3902 UK GPG: 7D025C00 -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
