Merge pull request #8933 from fricklerhandwerk/option-anchors

Add anchors to option listings
This commit is contained in:
John Ericson 2023-09-06 09:39:33 -04:00 committed by GitHub
commit 3a62651bd6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -98,7 +98,7 @@ let
(option ? labels) (option ? labels)
(concatStringsSep " " (map (s: "*${s}*") option.labels)); (concatStringsSep " " (map (s: "*${s}*") option.labels));
in trim '' in trim ''
- `--${name}` ${shortName} ${labels} - <span id="opt-${name}">[`--${name}`](#opt-${name})</span> ${shortName} ${labels}
${option.description} ${option.description}
''; '';