doc/style.css

   1 body {
   2     text-align: justify;
   3 }
   4
   5 div.body {
   6     margin: 0 auto;
   7     padding: 5%;
   8 }
   9
  10 h1 {
  11     text-align: center;
  12     font-size: 200%;
  13     font-style: normal;
  14     font-weight: bold;
  15 }
  16
  17 h2 {
  18     text-align: left;
  19     font-size: 150%;
  20     font-style: normal;
  21     font-weight: bold;
  22 }
  23
  24 h3 {
  25     text-align: left;
  26     font-size: 120%;
  27     font-style: normal;
  28     font-weight: bold;
  29 }
  30
  31 code {
  32     font-family: monospace;
  33     whitespace: pre;
  34     background-color: #afcfff;
  35     color: #000000;
  36 }
  37
  38 strong.since {
  39     border: 1pt solid;
  40     font-family: sans;
  41     font-size: 50%;
  42     font-weight: normal;
  43     padding: 1pt;
  44     vertical-align: middle;
  45 }
  46
  47 strong.since.current {
  48     border: 2pt solid;
  49     font-weight: bold;
  50 }
  51
  52 table th, td {
  53     border: none;
  54     text-align: left;
  55     vertical-align: top;
  56     padding: 0.2em 1em 0.2em 0.2em;
  57 }
  58 strong.since {
  59     border: 1pt solid;
  60     font-family: sans;
  61     font-size: 50%;
  62     font-weight: normal;
  63     padding: 1pt;
  64     vertical-align: middle;
  65 }
  66
  67 strong.since.current {
  68     border: 2pt solid;
  69     font-weight: bold;
  70 }