Add size option for terminal font
Current font size seems to be hardcoded to 12 pixels?
Making this configurable would also improve usage on smaller displays (smaller font -> more screen space).
I guess this can also be considered an extension of #10 (closed)