Patch #1215184: fileinput now has a fileno() function for getting the

current file number.