diff options
author | Eelco Dolstra <edolstra@gmail.com> | 2022-02-16 10:47:51 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-02-16 10:47:51 +0100 |
commit | f450edc78bd3dd4ad865b8d6f7f0f0b8afd01354 (patch) | |
tree | e3d249aa653cb313fb7d601d5fe931af00ca0d91 | |
parent | 94992a919636fb9df4c7441dacbde08592e4494d (diff) | |
parent | d82cf4a016aa0ee136ff62635e909607de78e02a (diff) |
Merge pull request #6104 from rrbutani/master
Fix formatting for options with "machine-specific" defaults
-rw-r--r-- | doc/manual/generate-options.nix | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/manual/generate-options.nix b/doc/manual/generate-options.nix index 9a77f4d36..84d90beb6 100644 --- a/doc/manual/generate-options.nix +++ b/doc/manual/generate-options.nix @@ -20,7 +20,7 @@ concatStrings (map # JSON, but that converts to "{ }" here. (if isAttrs option.value then "`\"\"`" else "`" + toString option.value + "`")) + "\n\n" - else " **Default:** *machine-specific*") + else " **Default:** *machine-specific*\n") + (if option.aliases != [] then " **Deprecated alias:** " + (concatStringsSep ", " (map (s: "`${s}`") option.aliases)) + "\n\n" else "") |