tweak raw_input style

more crowded, less jumpy
MinRK 13 years ago
parent ba79b60c35
commit 938a5b5dbc

@ -476,17 +476,27 @@ margin-bottom:0;
a.heading-anchor:link, a.heading-anchor:visited {
text-decoration: none;
color: inherit;
}
/* raw_input styles */
span.input_prompt {
div.raw_input {
padding-top: 0px;
padding-bottom: 0px;
height: 1em;
line-height: 1em;
font-family: monospace;
}
span.input_prompt {
font-family: inherit;
}
input.raw_input {
color: inherit;
width: auto;
height: 1em;
line-height: 1em;
margin: -2px 0px 0px 0px;
font-family: inherit;
font-size: inherit;
color: inherit;
width: auto;
margin: -2px 0px 0px 1px;
padding-left: 1px;
padding-top: 2px;
height: 1em;
}

Loading…
Cancel
Save