Specify encoding of text files

Under Windows, the default encoding is ISO 8859-1 (or CP-1252). Since Java reads files using the default OS encoding, if you edit UTF-8 files under Windows, they will be incorrectly interpreted by the program.

Solution: add a command line switch to specify the input encoding