I've found a couple of other bugs that I wanted to document here.
1. File.writeline('') does nothing.
File.writestring() writes a string to a file; File.writeline() also writes a string to a file, then adds a line separator (depending on the operating system).
File.writestring('') should do nothing BUT File.writeline('') should add a new line separator. Instead it does nothing.
For my purposes, File.writeline(' '); works fine but leaves me with a lot of extra spaces at the end of lines. You could also look up the separator for your system and File.writestring(separator) directly.
2. File.open(filename, 'write') doesn't truncate existing files.
If you open a file that already exists and write to it, but your new file is shorter than the existing file, you'll see the new data at the beginning - and then the rest of the old data after that!
Delete the old file by hand before overwriting it. Yes, annoying.
There seems to be no way to delete a file programmatically, or to truncate it when you close it.
3. The webpage documenting the File class has the wrong title!
It should be: The File object.
(It makes it hard to find the right page when Googling).