$INPUT_LINE: Line number that begins current section ¶‘$INPUT_LINE’ is the number of the line in the web source file
that begins the current section (not the source line in which the
$INPUT_LINE command appears). Compare $OUTPUT_LINE,
$OUTPUT_LINE: Current line number of tangled output.