Added optional encoding parameter to `io.open_file()`. Sometimes encoding auto-detection via `io.encodings` is more trouble than it's worth.
Added optional encoding parameter to `io.open_file()`.
Sometimes encoding auto-detection via `io.encodings` is more trouble than it's
worth.

rgieseke/textadept,rgieseke/textadept