header.sed - Echo the input stream up to the first empty line
NAME
NAME
header.sed - Echo the input stream up to the first empty line (usual end-of-header marker)
header.sed - Echo the input stream up to the first empty line