Bob, thanks for fixing the bug I reported! And good luck with getting GNU time 1.8 out :-)
I wrote: > rpm -q -f /usr/bin/time > util-linux-2.17.2-5.3.x86_64 Just curious: how will your fix reach util-linux because this is what distributions use (not GNU time directly, it seems)? Ciao Sven
