From 627bcb062651cca91c93a07042276146acbad75f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 18 Aug 2023 08:47:25 +0100 Subject: [PATCH] Remove extra spacing --- static/style.css | 2 -- 1 file changed, 2 deletions(-) diff --git a/static/style.css b/static/style.css index c6d6f68..a4adcde 100644 --- a/static/style.css +++ b/static/style.css @@ -701,13 +701,11 @@ pre code { padding: 0 0; } .inductive_ctor_doc { text-indent: 2ex; - padding-top: 1ex; font-family: 'Open Sans', sans-serif; } .structure_field_doc { text-indent: 0; - padding-top: 1ex; font-family: 'Open Sans', sans-serif; }