# Note that this script reads the file a line at a time (not a record at a time
# with a line ontaining "eof" as the record terminator).  This will work with
# any standards-conforming version of awk; while the other code you're using
# with RS set to "eof\n" only works on versions of awk that support
# multi-character record separator values (which is not required by the
# standards).
awk '
/eof/   {# For each input line that contains the string "eof"...
	 #	if the HR saved for this group is <= 12, print this record.
	 if (HR <= 12)   print TMP

	 # Clear the hold area for the current record and reset the delmiter to
	 # an empty string.
         TMP = DL = ""

	 # Read the next input line and skip the remaining steps in this script
	 # for this line.
         next
        }
        {# For every line in the input file (other than the "eof" lines we have
	 # discarded), add the current delimter and the current input line to
	 # the saved text containing the current record and set the delimiter to
	 # be used when adding later lines to this record to a comma.
	 TMP = TMP DL $0
         DL  = ","
        }
/^time/ {# For lines that start with the string "time", save two characters
	 # starting with the sixth character on this line in the variable HR.
	 # (I.e. set HR to the two digit hour from the "time" line.)
	 HR = substr ($0, 6, 2)
        }
' log	# End the awk script and specify that the file named "log" is to be
	# read as input.

         HR = substr ($0, 6, 2)

         HR = subset ($0, 6, 2) + 0