From c1a0f5a0408f1d744daeb6d43619240e1d6be179 Mon Sep 17 00:00:00 2001 From: rycee Date: Sat, 29 Jul 2023 17:44:17 +0000 Subject: [PATCH] deploy: f58889c07efa8e1328fdf93dc1796ec2a5c47f38 --- options.html | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/options.html b/options.html index e103512d..3572c2aa 100644 --- a/options.html +++ b/options.html @@ -4775,7 +4775,9 @@ boolean

Default: false

Example: true

Declared by:

<home-manager/modules/programs/gnome-terminal.nix> -
programs.gnome-terminal.profile

A set of Gnome Terminal profiles.

Type: +

programs.gnome-terminal.profile

A set of Gnome Terminal profiles. Note, the name of a profile must be +a UUID. You can generate one, for example, using uuidgen +(from util-linux).

Type: attribute set of (submodule)

Default: { }

Declared by:

<home-manager/modules/programs/gnome-terminal.nix>