Warn that coding style costs points.
[pintos-anon] / doc / pintos.css
1 body {
2         background: white;
3         color: black;
4         padding: 0em 1em 0em 3em;
5         margin: 0
6 }
7 body>p {
8         margin: 0pt 0pt 0pt 0em;
9         text-align: justify
10 }
11 body>p + p {
12         margin: .75em 0pt 0pt 0pt
13 }
14 H1 {
15         font-size: 150%;
16         margin-left: -1.33em
17 }
18 H2 {
19         font-size: 125%;
20         font-weight: bold;
21         margin-left: -.8em
22 }
23 H3 {
24         font-size: 100%;
25         font-weight: bold;
26         margin-left: -.5em }
27 H4 {
28         font-size: 100%;
29         margin-left: 0em
30 }
31 H1, H2, H3, H4, H5, H6 {
32         font-family: sans-serif;
33         color: blue
34 }
35 html {
36         margin: 0
37 }
38 code {
39         font-family: sans-serif
40 }
41
42 a:link {
43         color: blue;
44         text-decoration: none;
45 }
46 a:visited {
47         color: gray;
48         text-decoration: none;
49 }
50 a:active {
51         color: black;
52         text-decoration: none;
53 }
54 a:hover {
55         text-decoration: underline
56 }
57
58 address {
59         font-size: 90%;
60         font-style: normal
61 }
62
63 HR { 
64         display: none
65 }