diff options
author | Kevin Quick <kquick@galois.com> | 2020-09-24 22:41:24 -0700 |
---|---|---|
committer | Kevin Quick <kquick@galois.com> | 2020-09-24 22:41:24 -0700 |
commit | 83fec38fc93922192ada7c0409fec76578ef8dfb (patch) | |
tree | b77459fa0a60da4c496dbab4a65f0d5135a0d041 /doc | |
parent | a303c0b6dc71b1e0d6a57986c3f7a9b61361cd92 (diff) |
Update document generation for empty json object values.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/manual/generate-options.nix | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/doc/manual/generate-options.nix b/doc/manual/generate-options.nix index 7afe279c3..3c31a4eec 100644 --- a/doc/manual/generate-options.nix +++ b/doc/manual/generate-options.nix @@ -13,7 +13,12 @@ concatStrings (map then "*empty*" else if isBool option.value then (if option.value then "`true`" else "`false`") - else "`" + toString option.value + "`") + "\n\n" + else + # n.b. a StringMap value type is specified as a string, but + # this shows the value type. The empty stringmap is "null" in + # JSON, but that converts to "{ }" here. + (if isAttrs option.value then "`\"\"`" + else "`" + toString option.value + "`")) + "\n\n" + (if option.aliases != [] then " **Deprecated alias:** " + (concatStringsSep ", " (map (s: "`${s}`") option.aliases)) + "\n\n" else "") |