file.writelines()?

Bill Janssen (janssen@parc.xerox.com)
Fri, 22 Oct 1993 16:39:04 PDT

To write scripts, it would be handy to have something that lets one cat
a file to a file, something that's the equivalent of readlines(), but on
the output side (writelines()?), so that you could write

out.writelines(in.readlines())

Bill