From ab3365d57df52f7622b9d96adecf6c1a1e181b0d Mon Sep 17 00:00:00 2001
From: Paul-Elliot <peada@free.fr>
Date: Thu, 10 Mar 2022 18:29:48 +0100
Subject: [PATCH] Fix css of variant and record comments

Signed-off-by: Paul-Elliot <peada@free.fr>
---
 src/odoc/etc/odoc.css | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/odoc/etc/odoc.css b/src/odoc/etc/odoc.css
index 4cbbfffcbd..97a6f91b24 100644
--- a/src/odoc/etc/odoc.css
+++ b/src/odoc/etc/odoc.css
@@ -451,11 +451,12 @@ div.odoc-spec,.odoc-include {
 
 .spec.type .record > .def-doc, .spec.type .variant > .def-doc {
   min-width:50%;
-  padding-left: 22px;
+  padding: 0.25em 0.5em;
   margin-left: 10%;
   border-radius: 3px;
   flex-grow:1;
-  border-left: 0.1em solid var(--spec-summary-border-color);
+  background: var(--main-background);
+  box-shadow: 2px 2px 4px lightgrey;
 }
 
 div.def {