Skip to content

Commit

Permalink
fix: marginal notes now work better on narrow phone screens
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Nov 15, 2024
1 parent ef36ba9 commit ea10ba2
Showing 1 changed file with 27 additions and 16 deletions.
43 changes: 27 additions & 16 deletions Manual/Meta/Marginalia.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,30 +22,41 @@ def Marginalia.css := r#"
padding: 0.5rem;
}
/* Wide viewport */
@media (min-width: 1400px) {
.marginalia .note {
float: right;
clear: right;
margin-right: -19vw;
width: 15vw;
margin-top: 1rem;
}
@media screen and (min-width: 1400px) {
.marginalia .note {
float: right;
clear: right;
margin-right: -19vw;
width: 15vw;
margin-top: 1rem;
}
}
.marginalia:hover, .marginalia:hover .note, .marginalia:has(.note:hover) {
background-color: var(--lean-accent-light-blue);
}
/* Narrow viewport */
@media (max-width: 1400px) {
.marginalia .note {
float: right;
clear: right;
width: 40%;
margin: 1rem 0;
margin-left: 5%;
/* Medium viewport */
@media screen and (700px < width <= 1400px) {
.marginalia .note {
float: right;
clear: right;
width: 40%;
margin: 1rem 0;
margin-left: 5%;
}
}
/* Narrow viewport (e.g. phone) */
@media screen and (width <= 700px) {
.marginalia .note {
float: left;
clear: left;
width: 90%;
margin: 1rem 5%;
}
}
body {
counter-reset: margin-note-counter;
}
Expand Down

0 comments on commit ea10ba2

Please sign in to comment.