bash組み込みtimeの出力をリダイレクト

今日研究室の後輩から聞かれたことのメモ。
研究室の後輩に「bash組み込みコマンドのtimeの出力結果をファイルに落としたいんだけど、うまくリダイレクトできない、教えてくれ」、と尋ねられた。ちょっと確認したところ、標準エラーに出力されているようだったので、「2>&1」をつけて実行してみた。

 $ time COMMAND 2>&1 > output

だけど、COMMANDの出力結果はoutputに出力されたが、timeの出力はそのままコンソールに出力されてしまう。
ちょっと悩んだけど、bashのサブシェル機能(http://www.linux.or.jp/JM/html/GNU_bash/man1/bash.1.htmlを"(list)"で検索)を思い出し、以下のように使ってみたところ見事outputに出力された。

 $ (time COMMAND) 2>&1 > output

http://www.linux.or.jp/JM/html/GNU_bash/man1/bash.1.htmlを読んでみると、パイプラインの説明のところにこう書かれていた。

パイプライン (pipeline)は、記号 | で区切った 1 つ以上のコマンド列です。パイプラインのフォーマットを以下に示します:

[time [-p] ] [ ! ] command [ | command2 ... ]

(中略)

パイプラインの前に予約語 time がある場合、コマンドの実行にかかった経過時間・ユーザ時間・システム時間がパイプラインの終了時に報告されます。

コマンド1行がパイプラインに相当して、この仕様からすると、1行全て実行した後に時間が出力されるので、リダイレクトできないのもうなずける。直感でサブシェルを使ってみたんだけど、この方法で良かったんだと納得できて、ちょっと満足。