max@0
|
1 body
|
max@0
|
2 {
|
max@0
|
3 font-family: "Trebuchet MS", Trebuchet, "DejaVu Sans", "Luxi Sans", "Liberation Sans", Arial, Helvetica, sans-serif;
|
max@0
|
4 color: #000000;
|
max@0
|
5 background-color: #FFFFFF;
|
max@0
|
6 /* font-size: 10pt; */
|
max@0
|
7 /* line-height: 120%; */
|
max@0
|
8 height: 110%;
|
max@0
|
9 }
|
max@0
|
10
|
max@0
|
11 /* In the above, "height: 110%;" is a hack for stylistic purposes.
|
max@0
|
12 It typically makes the browser place a scroll bar on the left,
|
max@0
|
13 thereby reducing the overall width of the page. This is necessary,
|
max@0
|
14 as some pages do not have enough content (height wise) to make
|
max@0
|
15 the scrollbar appear, while other pages are long enough to have
|
max@0
|
16 the scrollbar. When content is centered for stylistic purposes,
|
max@0
|
17 the content on "short" pages will be in a different place than
|
max@0
|
18 the content on "long" pages. This can be visually annoying when
|
max@0
|
19 navigating from a "short" page to a "long" page, or vice versa.
|
max@0
|
20 Forcing the scrollbar to always appear removes this problem.
|
max@0
|
21 */
|
max@0
|
22
|
max@0
|
23 pre
|
max@0
|
24 {
|
max@0
|
25 font-family: "DejaVu Sans Mono", "Liberation Mono", "Andale Mono", "Bitstream Vera Sans Mono", "Luxi Mono", monospace;
|
max@0
|
26 font-size: smaller;
|
max@0
|
27 color: #666666;
|
max@0
|
28 }
|
max@0
|
29
|
max@0
|
30 a
|
max@0
|
31 {
|
max@0
|
32 text-decoration: none;
|
max@0
|
33 color: #57a706;
|
max@0
|
34 }
|
max@0
|
35
|
max@0
|
36 a:hover
|
max@0
|
37 {
|
max@0
|
38 text-decoration: underline;
|
max@0
|
39 color: #57a706;
|
max@0
|
40 }
|
max@0
|
41
|
max@0
|
42 a.menu
|
max@0
|
43 {
|
max@0
|
44 text-decoration: none;
|
max@0
|
45 color: #CCCCCC;
|
max@0
|
46 }
|
max@0
|
47
|
max@0
|
48 a.menu:hover
|
max@0
|
49 {
|
max@0
|
50 text-decoration: none;
|
max@0
|
51 color: #57a706;
|
max@0
|
52 }
|
max@0
|
53
|
max@0
|
54 a.hidden, a.hidden:hover, a.hidden:active, a.hidden:link, a.hidden:visited
|
max@0
|
55 {
|
max@0
|
56 text-decoration: none;
|
max@0
|
57 border-bottom: 0px
|
max@0
|
58 }
|
max@0
|
59
|
max@0
|
60 table
|
max@0
|
61 {
|
max@0
|
62 /* border: 1px solid #000; */
|
max@0
|
63 /* display: block; */
|
max@0
|
64 border-collapse: collapse;
|
max@0
|
65 }
|
max@0
|
66
|
max@0
|
67 td.line
|
max@0
|
68 {
|
max@0
|
69 border-left: 2px solid rgb(204, 204, 204);
|
max@0
|
70 }
|
max@0
|
71
|