output of Unix/Linux/*nix time (/usr/bin/time) into a file

I've encountered this problem before:

$ time somecommand arguments 2>&1 >> some_file.txt

real    0m0.001s
user    0m0.001s
sys     0m0.000s

And it drives me crazy. Why doesn't the program 'time' write its output to the, erm, 'normal' stdout or stderr, the ones I'm redirecting? Supposedly, you can use

 time -o outfile.txt somecommand arguments 

(or -a for append) to get the desired effect, but only on GNU time. And inexplicably, this doesn't work on most systems I've used.

Of course, if you Google for anything along the lines of 'time redirect i/o' you'll get a million matches to shell script tutorials saying "this time, we'll use I/O redirection..."

Eventually, I realized that Googling for "/usr/bin/time I/O redirect" got some useful results.

Well, if you're using non-GNU time, and you're using bash or sh (who knows, maybe even csh works this way?), you can do this:

$ ( time command arguments ) 2>> time.out > command.out

Which is a big ol' ugly hack, but it works.





UPDATE:


So the venerable aaron has informed me that I wasn't getting /usr/bin/time, I was getting the bash builtin command 'time' - hence

$env time
/usr/bin/time

and yet the command 'time' does not behave as expected. I should have seen that one coming. The obvious workaround is to explicitly call /usr/bin/time instead of time.

This strikes me as particularly frustrating as bash is a GNU project, and yet it's builtin 'time' does not behave like the 'real' GNU time, but ah well.