From d70c8b78f85d750557e52c63dff29c52a84feff9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 13 Nov 2023 23:13:26 +0100
Subject: [PATCH] fix: always keep a consistent font size

---
 static/style.css | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/static/style.css b/static/style.css
index fcb73d7..b10d3e2 100644
--- a/static/style.css
+++ b/static/style.css
@@ -21,6 +21,7 @@ a {
 
 h1, h2, h3, h4, h5, h6 {
     font-family: 'Lato Medium';
+    font-size: 17px;
 }
 
 body { line-height: 1.5; }
@@ -708,11 +709,13 @@ pre code { padding: 0 0; }
 .inductive_ctor_doc  {
     text-indent: 2ex;
     font-family: 'Lato Medium';
+    font-size: 17px;
 }
 
 .structure_field_doc {
     text-indent: 0;
     font-family: 'Lato Medium';
+    font-size: 17px;
 }
 
 .structure_ext_fields {