5a5a87d602
Calls '.flush()' on the contained 'ofstream' object. Needed as a means of ensuring that bits in the internal buffers of the I/O system are promptly output to permanent storage. This, in turn, is needed in upcoming work on the summary writing feature.