+++ /dev/null
-BODY{ background: white;
- color: black }
-
-A:link{ background: white;
- color: blue }
-A:visited{ background: white;
- color: rgb(50%, 0%, 50%) }
-
-H1{ background: white;
- color: rgb(55%, 55%, 55%);
- font-family: monospace;
- font-size: x-large;
- text-align: center }
-
-H2{ background: white;
- color: rgb(40%, 40%, 40%);
- font-family: monospace;
- font-size: large;
- text-align: center }
-
-H3{ background: white;
- color: rgb(40%, 40%, 40%);
- font-family: monospace;
- font-size: large }
-
-H4{ background: white;
- color: rgb(40%, 40%, 40%);
- font-family: monospace;
- font-style: italic;
- font-size: large }
-
-H5{ background: white;
- color: rgb(40%, 40%, 40%);
- font-family: monospace }
-
-H6{ background: white;
- color: rgb(40%, 40%, 40%);
- font-family: monospace;
- font-style: italic }
-
-IMG.toplogo{ vertical-align: middle }
-
-IMG.arrow{ width: 30px;
- height: 30px;
- border: 0 }
-
-span.acronym{font-size: small}
-span.env{font-family: monospace}
-span.file{font-family: monospace}
-span.option{font-family: monospace}
-span.pkg{font-weight: bold}
-span.samp{font-family: monospace}
-
-div.vignettes a:hover {
- background: rgb(85%, 85%, 85%);
-}
-