diff options
Diffstat (limited to 'userContent')
| -rw-r--r-- | userContent/reproducible/static/style.css | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/userContent/reproducible/static/style.css b/userContent/reproducible/static/style.css index df093045..5637ee7d 100644 --- a/userContent/reproducible/static/style.css +++ b/userContent/reproducible/static/style.css @@ -91,10 +91,6 @@ a.package:visited, a.noted:visited { font-size: 0.9em; } -ul.menu { - margin-bottom: 1em; -} - .head li { list-style: none; display: block !important; @@ -121,10 +117,8 @@ ul.menu { } -ul.reproducible-links { - margin-top: 1em; +ul.new-menu { border-top: 1px solid #eee; - padding-top: 0.5em; } ul.reproducible-links li { @@ -144,6 +138,7 @@ header { } header.head { + padding-top: 0.5em; background: #fafafa; } @@ -174,6 +169,9 @@ ul li { background-color: #bfeaff; } +.current { + font-weight: bold; +} h1 { font-size : 250%; @@ -197,6 +195,12 @@ h3 { font-size : 110%; } +h4 { + color: #d70a53; + font-size : 90%; + margin: 0.5em; +} + table { counter-reset: rowNumber; /* used for automatic row count with CSS */ border: 1px solid #ddd; @@ -435,7 +439,7 @@ span.dangerous { color: orange; } border: none; border-right: 1px solid #eee; height: 100%; - padding-top: 0px; + padding-top: 0.5em; overflow: auto; } .mainbody { |