doc/pintos.css

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