1body {
2    background: white;
3    color: black;
4}
5
6a:link {
7    background: white;
8    color: blue;
9}
10
11a:visited {
12    background: white;
13    color: rgb(50%, 0%, 50%);
14}
15
16h1 {
17    background: white;
18    color: rgb(55%, 55%, 55%);
19    font-family: monospace;
20    font-size: x-large;
21    text-align: center;
22}
23
24h2 {
25    background: white;
26    color: rgb(40%, 40%, 40%);
27    font-family: monospace;
28    font-size: large;
29    text-align: center;
30}
31
32h3 {
33    background: white;
34    color: rgb(40%, 40%, 40%);
35    font-family: monospace;
36    font-size: large;
37}
38
39h4 {
40    background: white;
41    color: rgb(40%, 40%, 40%);
42    font-family: monospace;
43    font-style: italic;
44    font-size: large;
45}
46
47h5 {
48    background: white;
49    color: rgb(40%, 40%, 40%);
50    font-family: monospace;
51}
52
53h6 {
54    background: white;
55    color: rgb(40%, 40%, 40%);
56    font-family: monospace;
57    font-style: italic;
58}
59
60img.toplogo {
61    width: 4em;
62    vertical-align: middle;
63}
64
65img.arrow {
66    width: 30px;
67    height: 30px;
68    border: 0;
69}
70
71span.acronym {
72    font-size: small;
73}
74
75span.env {
76    font-family: monospace;
77}
78
79span.file {
80    font-family: monospace;
81}
82
83span.option{
84    font-family: monospace;
85}
86
87span.pkg {
88    font-weight: bold;
89}
90
91span.samp{
92    font-family: monospace;
93}
94
95div.vignettes a:hover {
96    background: rgb(85%, 85%, 85%);
97}
98