Merge pull request #232 from kit-ty-kate/improve-ui-1

UI: Hide full results by default
ocurrent · Sep 5, 2023 · ab86f27 · ab86f27
2 parents f31b0a3 + 1f3ae1a
commit ab86f27
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/web-ui/github.ml b/web-ui/github.ml
@@ -211,8 +211,9 @@ let link_jobs ~owner ~name ~hash ?selected jobs =
     ]
   in
   error_tree @ [
-    h2 [txt "Full results"];
-    full_tree
+    details
+      (summary [b [txt "Full results"]])
+      [full_tree]
   ]
 
 let short_hash = Astring.String.with_range ~len:6