diff options
Diffstat (limited to 'scripts/gen_help_html.lua')
-rw-r--r-- | scripts/gen_help_html.lua | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/scripts/gen_help_html.lua b/scripts/gen_help_html.lua index c89a7c70da..f741efcaeb 100644 --- a/scripts/gen_help_html.lua +++ b/scripts/gen_help_html.lua @@ -944,6 +944,7 @@ local function gen_css(fname) padding-top: 10px; padding-bottom: 10px; } + .old-help-para { padding-top: 10px; padding-bottom: 10px; @@ -953,6 +954,12 @@ local function gen_css(fname) font-size: 16px; font-family: ui-monospace,SFMono-Regular,SF Mono,Menlo,Consolas,Liberation Mono,monospace; } + .old-help-para pre { + /* All text in .old-help-para is formatted as "white-space:pre" so text following <pre> is + already visually separated by the linebreak. */ + margin-bottom: 0; + } + a.help-tag, a.help-tag:focus, a.help-tag:hover { color: inherit; text-decoration: none; @@ -1006,6 +1013,9 @@ local function gen_css(fname) font-size: 16px; margin-top: 10px; } + pre:last-child { + margin-bottom: 0; + } pre:hover, .help-heading:hover { overflow: visible; |