On Friday, 24 April 2015 at 15:46:15 UTC, Adam D. Ruppe wrote:
Try terminal.writef("%s", cast(char) your_ascii_character); it should work.
Thank you, it works for the standard ascii characters but not the extended set - maybe that has something to do with my terminal settings...? (not that I know how to change them anyway!)
Paul