Joule,I would like to comment on another small issue that I think is malfunctioning in the terminal.
Copy any text, CTRL + C or with the mouse.
CTRL + F to open Find & Replace
Use the mouse to paste the copied text.
For some reason the entire pull-down menu does not work within Find & Replace (it is not possible to select, copy or paste with the mouse.). Butin the menu just the line that refers to the access Find & Replace is unchecked as an optionsomething that does not happen if you use the top box to program.
If in the end the terminal is improved in a future version, add a text zoom, please !!!
Your case and mine does not work well in R3.1.1 x64.
I am sorry not to open another issue with this issue, but I feel that it will be another issue in the drawer of oblivion.