gui: optionally set focus to console when a command is run from another widget * settings-dialog.ui: new checkbox for focus switching to console * settings-dialog.cc (constructor): read new setting and init check box, (write_changed_settings): write state from check box into settings file * main-window.cc (focus_console_after_command): new functions checking settings file for new settings, (execute_command_in_terminal): focus console if desired, (run_file_in_terminal): focus console if desired * main-window.h: new function focus_console_after_command

6d4e36653a40da6604507406f2a97e3e64bf9dbf gnulib-hg