-/* Write LENGTH characters in TEXT to file F, escaping characters
- as necessary for HTML. Spaces are replaced by SPACE, which
- should be " " or " ". */
+/* Write LENGTH characters in TEXT to file F, escaping characters as necessary
+ for HTML. Spaces are replaced by SPACE, which should be " " or " "
+ New-lines are replaced by NEWLINE, which might be "<BR>" or "\n" or
+ something else appropriate. */