diff --git a/docs/pandoc_templates/style.css b/docs/pandoc_templates/style.css index 86c7240..a54f73e 100644 --- a/docs/pandoc_templates/style.css +++ b/docs/pandoc_templates/style.css @@ -1,7 +1,7 @@ body { max-width: 30em; margin-left: 1em; - font-family: "DejaVu Serif, Georgia, Times New Roman", Times, serif; + font-family:"DejaVu Serif", "Georgia", serif; font-style: normal; font-variant: normal; font-weight: normal; @@ -16,8 +16,6 @@ td, th { padding: 0.5rem; text-align: left; } -code{white-space: pre-wrap; - } span.smallcaps{font-variant: small-caps; } span.underline{text-decoration: underline; @@ -45,13 +43,17 @@ td, th { text-align: left; } pre.terminal_image { - font-family: 'DejaVu Sans Mono, Lucida Console, sans-serif'; - background-color: #000; + background-color: #000; color: #0F0; - font-size: 75%; - white-space: no-wrap; - } + overflow: auto; + } +pre.terminal_image > code { white-space: pre; position: relative; + } +pre.text { overflow: auto; } +pre.text > code { white-space: pre; } +code {font-family: "DejaVu Sans Mono", "Lucida Console", "sans-serif";} + * { box-sizing: border-box;} .logo-header {