index.css

   1 html            { min-width: 40em;
   2                   margin-top: 2em;
   3                   margin-left: auto;
   4                   margin-right: auto;
   5                   width: 80%; }
   6
   7 body            { text-align: justify;
   8                   font-family: Helvetica,Arial,sans-serif;
   9                   line-height: 120%;
  10                   font-size: small; }
  11
  12 p,ul,table      { margin-left: 3em; }
  13
  14 p.head,
  15 p.subhead,
  16 p.foot          { margin-left: 0.0em; margin-right: 0.0em; }
  17
  18 p.news          { margin-left: 2.0em; }
  19
  20 li              { margin: 0.25em; }
  21
  22 h1              { font-size: 110%; }
  23 h2              { font-size: 105%; margin-left: 1.5em }
  24
  25 p.head          { margin-bottom: 0.5em;
  26                   border-bottom: 1px solid #dddddd;
  27                   padding-bottom: 0.2em; }
  28
  29 p.subhead       { margin-top: 0em;
  30                   margin-bottom: 1.75em; }
  31
  32 p.foot          { border-top: 1px solid #dddddd;
  33                   color: #666666;
  34                   padding-top: 0.2em;
  35                   margin-top: 1.75em; }
  36
  37 span.nm         { color: green; }
  38
  39 span.file       { font-style: italic; }
  40
  41 span.attn       { font-weight: bold; }
  42
  43 span.flag       { font-weight: bold; }
  44
  45 a               { text-decoration: none; }
  46
  47 a.external      { background: transparent url(external.png) center right no-repeat;
  48                   padding-right: 12px; }