/* General Fonts */ html, body, div, p { font-family: DejaVu Sans, Verdana, Arial, sans-serif; font-size: 12pt; color: $text-color; } /* Links */ a { text-decoration: none; color: $link-color; } a:hover, a:focus { text-decoration: underline; } /* Header Size & Spacing */ h1, h2, h3, h4 { color: $text-color; a { color: $text-color; } } h1 { margin-top: 0.1em; font-size: 200%; margin-bottom: 0.2em; } h2 { margin-top: 0.5em; font-size: 150%; margin-bottom: 0.2em; } h3 { margin-top: 0.5em; font-size: 130%; margin-bottom: 0.1em; } h4 { margin-top: 0.5em; font-size: 110%; margin-bottom: 0.0em; } /* Content styling */ .side, .comment { color: $light-text-color; a { color: $light-link-color; } } figure { margin: 0; } pre, code { background-color: $code-background-color; font-family: monospace; font-size: 82%; } code { padding: 0.1em 0.2em; } pre { padding: 0.6em; } pre code { padding: 0; font-size: 100%; } p { margin: 0.5em 0; line-height: 1.3; } .comment { margin-top: 1.5em; }