Paul Jackson Wed, 23 Aug 2023 01:24:10 -0700
oops - grep slower than awk, not the other way around, on these _highly_ inconclusive timings.
-- Paul Jackson p...@usa.net