From e888e9cc383f838ef8f519e6941e32fe5c48df1b Mon Sep 17 00:00:00 2001 From: Henrik Date: Thu, 11 May 2023 22:36:27 +0200 Subject: [PATCH] feat: doc strings on ctors and fields are not monospaced anymore --- static/style.css | 2 ++ 1 file changed, 2 insertions(+) diff --git a/static/style.css b/static/style.css index 8135090..1eecef1 100644 --- a/static/style.css +++ b/static/style.css @@ -539,11 +539,13 @@ 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; } .structure_ext_fields {