[BLUEJ-177] Terminal options should persist across sessions
The terminal options, accessible through the Terminal 'Options' menu, should be saved with user preferences, so that they are retained across different sessions.
Issue metadata
- Issue type: Task
- Priority: Low
- Fix versions: 3.0.0