1
0
Fork 0
mirror of https://github.com/nix-community/home-manager synced 2024-11-30 06:59:45 +01:00

bash: add option historyFile

This commit is contained in:
John Wiegley 2018-01-06 01:10:20 -08:00 committed by Robert Helgesson
parent d7715f71ad
commit c9294e30d9
No known key found for this signature in database
GPG key ID: C3DB11069E65DC86

View file

@ -21,6 +21,12 @@ in
description = "Number of history lines to keep in memory.";
};
historyFile = mkOption {
type = types.str;
default = "$HOME/.bash_history";
description = "Location of the bash history file.";
};
historyFileSize = mkOption {
type = types.int;
default = 100000;
@ -136,8 +142,9 @@ in
historyControlStr =
concatStringsSep "\n" (mapAttrsToList (n: v: "${n}=${v}") (
{
HISTSIZE = toString cfg.historySize;
HISTFILE = "\"${cfg.historyFile}\"";
HISTFILESIZE = toString cfg.historyFileSize;
HISTSIZE = toString cfg.historySize;
}
// optionalAttrs (cfg.historyControl != []) {
HISTCONTROL = concatStringsSep ":" cfg.historyControl;