diff --git a/index.html b/index.html index e1350e92..dbf54f35 100644 --- a/index.html +++ b/index.html @@ -1,6 +1,6 @@ -
ca.desrt.dconf
or dconf.service
?+
ca.desrt.dconf
or dconf.service
?This manual will eventually describe how to install, use, and extend Home Manager.
diff --git a/options.html b/options.html index a4349d6c..5e54a1f9 100644 --- a/options.html +++ b/options.html @@ -905,7 +905,7 @@ is assumed to already be available in your profile.
Type: string
Example: "DejaVu Sans"
Declared by:
<home-manager/modules/misc/gtk.nix>
|
gtk.font.size
The size of the font. -
Type: null or signed integer
Default: null
Example: "8"
Declared by:
+ |