#! /usr/bin/gawk -f
# Last edited on 2003-09-05 14:52:40 by stolfi

BEGIN { nl=0; nb=0; hdr=""; }

/^From / { 
  if (hdr != "") { printf "%7d %8d %s\n", nl, nb, hdr; }
  hdr=$0; nl=0; nb=0; }

// { nl++; nb += (length($0)+1); next; }

END { if (hdr != "") { printf "%7d %8d %s\n", nl, nb, hdr; } }