1 BODY{ background: white;
4 A:link{ background: white;
6 A:visited{ background: white;
7 color: rgb(50%, 0%, 50%) }
10 color: rgb(55%, 55%, 55%);
11 font-family: monospace;
15 H2{ background: white;
16 color: rgb(40%, 40%, 40%);
17 font-family: monospace;
21 H3{ background: white;
22 color: rgb(40%, 40%, 40%);
23 font-family: monospace;
26 H4{ background: white;
27 color: rgb(40%, 40%, 40%);
28 font-family: monospace;
32 H5{ background: white;
33 color: rgb(40%, 40%, 40%);
34 font-family: monospace }
36 H6{ background: white;
37 color: rgb(40%, 40%, 40%);
38 font-family: monospace;
41 IMG.toplogo{ vertical-align: middle }
43 IMG.arrow{ width: 30px;
47 span.acronym{font-size: small}
48 span.env{font-family: monospace}
49 span.file{font-family: monospace}
50 span.option{font-family: monospace}
51 span.pkg{font-weight: bold}
52 span.samp{font-family: monospace}
54 div.vignettes a:hover {
55 background: rgb(85%, 85%, 85%);