From 8c165b15702b2c60f2770acf9f1a62ef631a6692 Mon Sep 17 00:00:00 2001 From: Ben Radford Date: Tue, 20 Feb 2024 14:11:38 +0000 Subject: [PATCH] Minor tweaks to style. --- backend/src/Render.hs | 2 +- frontend/src/theme.css | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/backend/src/Render.hs b/backend/src/Render.hs index f96ab9f..1ef13d8 100644 --- a/backend/src/Render.hs +++ b/backend/src/Render.hs @@ -103,7 +103,7 @@ renderGraph database dbPath nodeStates = do <> graphvizAttributes [ ("arrowsize", "0.5"), ("color", "#3f3f3f"), - ("penwidth", "0.2") + ("penwidth", "0.4") ], Text.unlines $ uncurry graphvizNode <$> Map.assocs nodeMap, Text.unlines $ graphvizEdge [] <$> edges, diff --git a/frontend/src/theme.css b/frontend/src/theme.css index 0ed960b..333bb5e 100644 --- a/frontend/src/theme.css +++ b/frontend/src/theme.css @@ -431,6 +431,7 @@ div.Popup.Pinned > div.Content > p { overflow: auto; white-space: pre; margin: 3px 5px; + min-height: 30px; } div.Popup.Pinned {