brl/gnome-shell
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

run-dialog: Use user preference when executing in terminal

Browse Source 
Rather than hardcoding gnome-terminal, pick up the user's preferred
terminal from System Settings.

https://bugzilla.gnome.org/show_bug.cgi?id=648422
This commit is contained in:
Florian Müllner 2011-06-01 13:39:11 +02:00
parent 7b65735cc9
commit aa4dbee362
1 changed files with 10 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
js/ui/runDialog.js
View File

@ -23,6 +23,10 @@ const HISTORY_KEY = 'command-history';
const LOCKDOWN_SCHEMA = 'org.gnome.desktop.lockdown';
const DISABLE_COMMAND_LINE_KEY = 'disable-command-line';
const TERMINAL_SCHEMA = 'org.gnome.desktop.default-applications.terminal';
const EXEC_KEY = 'exec';
const EXEC_ARG_KEY = 'exec-arg';
const DIALOG_GROW_TIME = 0.1;
function CommandCompleter() {
@ -169,6 +173,7 @@ __proto__: ModalDialog.ModalDialog.prototype,
ModalDialog.ModalDialog.prototype._init.call(this, { styleClass: 'run-dialog' });
this._lockdownSettings = new Gio.Settings({ schema: LOCKDOWN_SCHEMA });
this._terminalSettings = new Gio.Settings({ schema: TERMINAL_SCHEMA });
global.settings.connect('changed::development-tools', Lang.bind(this, function () {
this._enableInternalCommands = global.settings.get_boolean('development-tools');
}));
@ -309,8 +314,11 @@ __proto__: ModalDialog.ModalDialog.prototype,
f();
} else if (input) {
try {
if (inTerminal)
command = 'gnome-terminal -x ' + input;
if (inTerminal) {
let exec = this._terminalSettings.get_string(EXEC_KEY);
let exec_arg = this._terminalSettings.get_string(EXEC_ARG_KEY);
command = exec + ' ' + exec_arg + ' ' + input;
}
Util.trySpawnCommandLine(command);
} catch (e) {
// Mmmh, that failed - see if @input matches an existing file