/* Write 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. */
/* Write 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. */