1
0
Fork 0
mirror of https://github.com/nix-community/home-manager synced 2024-12-24 02:39:48 +01:00

gnome-terminal: add profile command options

Allow setting custom command and login shell.

PR #1423
This commit is contained in:
Jack McCown 2020-08-01 19:57:42 -04:00 committed by Robert Helgesson
parent 96e2f1bdf0
commit 2a54c353a9
No known key found for this signature in database
GPG key ID: 36BDAA14C2797E89

View file

@ -122,6 +122,20 @@ let
The number of scrollback lines to keep, null for infinite.
'';
};
customCommand = mkOption {
default = null;
type = types.nullOr types.str;
description = ''
The command to use to start the shell, or null for default shell.
'';
};
loginShell = mkOption {
default = false;
type = types.bool;
description = "Run command as a login shell.";
};
};
});
@ -132,7 +146,13 @@ let
scrollback-lines = pcfg.scrollbackLines;
cursor-shape = pcfg.cursorShape;
cursor-blink-mode = pcfg.cursorBlinkMode;
} // (if (pcfg.font == null) then {
login-shell = pcfg.loginShell;
} // (if (pcfg.customCommand != null) then {
use-custom-command = true;
custom-command = pcfg.customCommand;
} else {
use-custom-command = false;
}) // (if (pcfg.font == null) then {
use-system-font = true;
} else {
use-system-font = false;