Minor tweaks to style.

tweag · Feb 20, 2024 · 8c165b1 · 8c165b1
1 parent dacb132
commit 8c165b1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -431,6 +431,7 @@ div.Popup.Pinned > div.Content > p {
     overflow: auto;
     white-space: pre;
     margin: 3px 5px;
+    min-height: 30px;
 }
 
 div.Popup.Pinned {