Joe Smith wrote:
...
$ time grep cat /usr/share/dict/words | grep red | wc
80 80 1082
real 0m0.051s
user 0m0.017s
sys 0m0.019s
...
And before some wise guy points out that only times the first grep, it makes very little difference:
$ time sh -c "grep cat /usr/share/dict/words | grep red | wc"
80 80 1082
real 0m0.059s
user 0m0.017s
sys 0m0.021s
Anyway, piping stuff around is more efficient than you might think.
<Joe
