4 font-family: Verdana, Arial, Helvetica, sans-serif;
9 border-top: 5px solid #DECD40;
10 border-bottom: 1px solid #AF9D00;
11 background: url(logo-head.png) top left no-repeat;
12 background-color: #EDE497;
19 background-color: #DECD40;
20 border-bottom: 1px solid #AF9D00;
32 background-color: #EDE497;
40 padding: 0 10px 10px 0;
41 border-bottom: 1px solid #AF9D00;
45 /* need non-zero top padding here to prevent margin propagation */
46 padding: 10px 0 0 142px;
52 text-decoration: none;
55 a:contains("http://") {
64 display: inline; /* IE double margin fix */
67 background-color: #FDF7C3;
68 border: 1px solid #AF9D00;
69 margin: 0 0 10px -132px;
75 margin-bottom: 0; /* Grmpf .. IE6 is f**ing up ... */
81 list-style-type: none;
93 text-decoration: none;
98 div.tabs ul li a:visited, div.tabs ul li a:active {
100 text-decoration: none;
103 div.tabs ul li a:hover, div.tabs ul li#current a {
105 text-decoration: none;
106 background-color: #EDE497;
111 padding: 4px 10px 4px 142px;
122 #footer a, #footer a:active, #footer a:visited {
124 text-decoration: none;
128 background-color: inherit;
129 text-decoration: underline;
133 border: 1px solid #AADD88;
134 background-color: #EEFFDD;
139 border: 1px solid #DDAA88;
140 background-color: #FFEEDD;
145 border: 1px solid A0C2C2;
146 background-color: #F0F8F8;
153 border: 1px solid #AAAAAA;
159 border: 2px solid white;
160 background-color: #EEEEEE;
166 background-color: #DDDDDD;
171 dl.bug, dl.fixme, dl.todo, dl.idea {
172 border: 1px solid #EE0000;
173 border-left-width: 4px;
174 background-color: #FFDDDD;
178 dl.xref-bug, dl.xref-fix, dl.xref-todo, dl.xref-idea {
179 border: 1px solid #CC8888;
182 background-color: #FFEEEE;
188 dl.xref-bug dt, dl.xref-fix dt, dl.xref-todo dt, dl.xref-idea dt,
189 dl.xref-bug dd, dl.xref-fix dd, dl.xref-todo dd, dl.xref-idea dd {
195 dl.xref-bug a, dl.xref-fix a, dl.xref-todo a, dl.xref-idea a {
200 border-color: #EEEE00;
201 background-color: #FFFFDD;
205 border-color: #CCCC88;
206 background-color: #FFFFEE;
210 border-color: #00AA00;
211 background-color: #DDFFDD;
215 border-color: #88CC88;
216 background-color: #EEFFEE;
220 border-color: #AAAAAA;
221 background-color: #EEEEEE;
225 border-color: #CCCCCC;
226 background-color: #F8F8F8;
239 background-color: white;
241 border-bottom: 1px solid #AF9D00;
248 background-color: #e8eef2;
249 border: 1px solid #84b0c7;