end-write-header-footer-to-file in editor<%>

This method must be called after writing any special header data to a stream.

• (send an-editor end-write-header-footer-to-file f buffer-value) -> void
     f : editor-stream-out% object
     buffer-value : exact integer

  The buffer-value argument must be the value put in the buffer argument box by begin-write-header-footer-to-file.

  See File Formats and write-headers-to-file for more information.