#! /usr/bin/gawk -f
# Last edited on 2003-03-03 00:15:47 by stolfi

/[.]ps/ {
  lin = $0;
  gsub(/[ ]/, "", lin);
  while(match(lin, /href="[^:"]*[.]ps([.]gz|)/))
    { lin = substr(lin, RSTART+6);
      if (! match(lin, /^[^"]+["]/)) { error(("bad file ref")); }
      file = substr(lin, 1, RLENGTH-1);
      lin = substr(lin, RLENGTH+1);
      print file;
    }
  next
}

// {
  next;
}

function error(msg)
{
  printf "file %s, line %s: %s\n", FILENAME, FNR, msg > "/dev/stderr";
  abort = 1;
  exit abort;
}