From c926985047cc18ea03809939f9028a2e35d9c140 Mon Sep 17 00:00:00 2001 From: github-deploy-action Date: Fri, 10 Nov 2023 05:26:18 +0000 Subject: [PATCH] github-deploy-action-dev --- dev/style.css | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/dev/style.css b/dev/style.css index 6a646dc1..a8ea7bca 100644 --- a/dev/style.css +++ b/dev/style.css @@ -1517,6 +1517,7 @@ svg.expandable path { } .result { + padding-top: 0.1em; min-height: 1.6em; width: 100%; overflow-y: hidden; @@ -1548,8 +1549,6 @@ svg.expandable path { .DHCode svg.err-hole { fill: #d001; - transform: scaleY(0.8); - /* HACK(andrew) */ stroke-dasharray: 1, 1; stroke: var(--err-color); stroke-width: 1.2px;