Even cleaner exiting of the GUI - the interpreter thread is terminated by the exit_gui() method.
Authored by: bugman 2012-10-15
Parent: [r17815]
Child: [r17817]
