version 1.30, 2018/05/26 17:38:01 |
version 1.31, 2018/05/26 20:04:41 |
|
|
.Li { font-style: normal; |
.Li { font-style: normal; |
font-weight: normal; |
font-weight: normal; |
font-family: monospace; } |
font-family: monospace; } |
|
|
|
/* Overrides to avoid excessive margins on small devices. */ |
|
|
|
@media (max-width: 37.5em) { |
|
div.manual-text { |
|
margin-left: 0.5em; } |
|
h1.Sh, h2.Ss { margin-left: 0em; } |
|
div.D1 { margin-left: 2em; } |
|
dl.Bl-hang > dd { |
|
margin-left: 2em; } |
|
dl.Bl-tag { margin-left: 2em; } |
|
dl.Bl-tag > dt { |
|
margin-left: -2em; } |
|
} |