From c73e071fcb69af0088986fb74629cb186b9b29bb Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 20 Sep 2023 16:48:23 +0200 Subject: [PATCH] Remove vertical margin when screen is half width This margin might have been useful to accomodate the side bar but is now unecessary. --- src/html_support_files/odoc.css | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/html_support_files/odoc.css b/src/html_support_files/odoc.css index a3317f33b0..0355236894 100644 --- a/src/html_support_files/odoc.css +++ b/src/html_support_files/odoc.css @@ -246,10 +246,9 @@ body { } body { - margin-left: calc(10vw + 20ex); - margin-right: 4ex; - margin-top: 20px; - margin-bottom: 50px; + margin-left: auto; + margin-right: auto; + padding: 0 4ex; } body.odoc {