Skip to content

Commit

Permalink
Remove vertical margin when screen is half width
Browse files Browse the repository at this point in the history
This margin might have been useful to accomodate the side bar but is now
unecessary.
  • Loading branch information
Julow committed Sep 20, 2023
1 parent 54b200c commit 05129a0
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/html_support_files/odoc.css
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -835,6 +834,7 @@ td.def-doc *:first-child {
@media only screen and (max-width: 110ex) {
body {
margin: 2em;
padding: 0;
}

body.odoc {
Expand Down

0 comments on commit 05129a0

Please sign in to comment.