Gnome Terminal needs nasty hack

[hedgeberg]

Gnome Terminal recently deprecated the -c option, opting instead for syntax of the style:

gnome-terminal -- /usr/bin/gdb ./target_binary 

to get around this, I had to make the following hack in utils/misc.py:

First, right below "if not terminal: ..." add:

if("gnome-terminal" in terminal):
    command = command.split(' ')

Then, change

argv = [terminal_path] + args + [command]

to

if("gnome-terminal" in terminal):
    argv = [terminal_path] + args + command
else:
    argv = [terminal_path] + args + [command]

Works, and should still support any other terminals. I am unsure if there are other terminals that might use the "-- [passed command line]" but I have a feeling there are, and it would be potentially worth it to add support.