diff --git a/index.html b/index.html index f1f1bfa7..81d5f584 100644 --- a/index.html +++ b/index.html @@ -1,6 +1,6 @@ -
ca.desrt.dconf
?+
ca.desrt.dconf
?This manual will eventually describes how to install, use, and extend Home Manager.
diff --git a/options.html b/options.html index 90f3da78..ea288586 100644 --- a/options.html +++ b/options.html @@ -3215,6 +3215,10 @@ presses the Backspace key.
Type: one of "auto", "ascii-backspace", "ascii-delete", "delete-sequence", "tty"
Default:
"ascii-delete"
+
Declared by:
+ <home-manager/modules/programs/gnome-terminal.nix>
+ |
programs.gnome-terminal.profile.<name>.boldIsBright
Whether bold text is shown in bright colors.
Type: null or boolean
Default:
+ null
Declared by:
<home-manager/modules/programs/gnome-terminal.nix>
|
programs.gnome-terminal.profile.<name>.colors
The terminal colors, null to use system default.
Type: null or submodule
Default:
@@ -3301,6 +3305,10 @@ presses the Delete key.
<home-manager/modules/programs/gnome-terminal.nix>
programs.gnome-terminal.profile.<name>.showScrollbar
Whether the scroll bar should be visible.
Type: boolean
Default:
true
+
Declared by:
+ <home-manager/modules/programs/gnome-terminal.nix>
+ |
programs.gnome-terminal.profile.<name>.transparencyPercent
Background transparency in percent.
Type: null or integer between 0 and 100 (both inclusive)
Default:
+ null
Declared by:
<home-manager/modules/programs/gnome-terminal.nix>
|
programs.gnome-terminal.profile.<name>.visibleName
The profile name.
Type: string
Declared by: