From 438b348218b9d577f4bfa5891234e005c2e92f10 Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 18 Dec 2024 18:16:06 +0100 Subject: [PATCH] css: Tweak number line color in source code pages --- src/html_support_files/odoc.css | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index 64478369e2..9fc310a982 100644 --- a/src/html_support_files/odoc.css +++ b/src/html_support_files/odoc.css @@ -230,7 +230,7 @@ --source-line-column: var(--fg3); - --source-line-column-bg: var(--bg1); + --source-line-column-bg: var(--bg_h); --source-code-comment: var(--gray); --source-code-docstring: var(--green-dim);