Merge pull request #7190 from patricksjackson/fix-defaults

Fix default values in the manual
This commit is contained in:
Théophane Hufschmitt 2022-10-25 16:48:59 +02:00 committed by GitHub
commit c7414d48f2
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -11,16 +11,16 @@ concatStrings (map
+ concatStrings (map (s: " ${s}\n") (splitLines option.description)) + "\n\n"
+ (if option.documentDefault
then " **Default:** " + (
if option.value == "" || option.value == []
if option.defaultValue == "" || option.defaultValue == []
then "*empty*"
else if isBool option.value
then (if option.value then "`true`" else "`false`")
else if isBool option.defaultValue
then (if option.defaultValue then "`true`" else "`false`")
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 isAttrs option.defaultValue then "`\"\"`"
else "`" + toString option.defaultValue + "`")) + "\n\n"
else " **Default:** *machine-specific*\n")
+ (if option.aliases != []
then " **Deprecated alias:** " + (concatStringsSep ", " (map (s: "`${s}`") option.aliases)) + "\n\n"