#! /usr/bin/gawk -f
# Last edited on 2003-10-12 12:35:03 by stolfi

/./{
  if ((NF != 5) || ($4 != "/")) { printf "Ħbad format!" >> "/dev/stderr"; }
  printf "%03d / %03d", ($1 * 0.30 + $2 * 0.60 + $3 * 0.10), $5;
}