From b7bf6f83f71f930c52bc6a0c47a89b9631da5d58 Mon Sep 17 00:00:00 2001 From: Henrik Levkowetz Date: Sat, 4 Apr 2015 19:48:33 +0000 Subject: [PATCH] Tweaked the pre text font. - Legacy-Id: 9402 --- static/css/ietf.css | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/static/css/ietf.css b/static/css/ietf.css index 81043a020..2e08b338d 100644 --- a/static/css/ietf.css +++ b/static/css/ietf.css @@ -154,8 +154,13 @@ label.required:after { content: "\2217"; color: #a94442; font-weight: bold; } /* Add some padding when there are multiple buttons in a line than can wrap. */ .buttonlist .btn { margin-bottom: .5em } -/* Make preformatted text a bit more condensed in display */ -pre { line-height: 1.214; } + +pre { + /* Make preformatted text a bit more condensed in display */ + line-height: 1.214; + /* PT Mono doesn't need the default one-step size reduction provided by bootstrap */ + font-size: 14px; +} /* Make ampersands pretty */ /* This sets ampersand in a different font than the rest of the text. Fancy, but it's