#!/usr/bin/awk -f

{ printf "%5d\t%s\n", NR, $0; }