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.