From 8b3cf2a9fc7dc02b1d77f2e118f951e505a48eba Mon Sep 17 00:00:00 2001
From: Lars Eggert <lars@eggert.org>
Date: Wed, 13 Jul 2022 14:22:08 -0700
Subject: [PATCH] fix(ui): Make the heading and textarea font sizes a bit
 smaller (#4212)

* ui: Make the heading and textarea font sizes a bit smaller

* Address review commit from @NGPixel
---
 ietf/static/css/ietf.scss | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/ietf/static/css/ietf.scss b/ietf/static/css/ietf.scss
index 2873b5a70..0720c2291 100644
--- a/ietf/static/css/ietf.scss
+++ b/ietf/static/css/ietf.scss
@@ -17,6 +17,13 @@ $popover-max-width: 100%;
 @import "bootstrap/scss/mixins";
 @import "bootstrap/scss/utilities";
 
+$h1-font-size: $font-size-base * 2.2;
+$h2-font-size: $font-size-base * 1.8;
+$h3-font-size: $font-size-base * 1.6;
+$h4-font-size: $font-size-base * 1.4;
+$h5-font-size: $font-size-base * 1.2;
+$h6-font-size: $font-size-base;
+
 // Layout & components
 @import "bootstrap/scss/root";
 @import "bootstrap/scss/reboot";
@@ -71,9 +78,10 @@ html {
     scroll-padding-top: 60px;
 }
 
-// Make textareas use a monospace font
-textarea {
-    font-family: var(--bs-font-monospace);
+// Make textareas in forms use a monospace font
+textarea.form-control {
+    font-family: $font-family-code;
+    font-size: $code-font-size;
 }
 
 // Wrap long lines in preformatted text.