source: trunk/scripts/invirt.mit.edu/static/style.css @ 2020

/*
  Good style ideas stolen from Debathena.
  Hey, we use some different fonts.
  And the colors are unmistakably different.
*/

/* Basic fonts and sizes. */
html {
    font-size: 87.5%;
}
body {
    font-family: Tahoma, Sans, sans-serif;
}
pre, code, samp, kbd, tt {
    font-family: "Bitstream Vera Sans Mono", "Luxi Mono", "Courier New", monospace;
    font-size: 100%;
}

/* Blue headings. */
h1, h2, h3, h4, h5, h6 {
    color: #246;
}

/* Dividing line under the header. */
h1 {
    border-bottom: 1px solid black;
    margin-top: 0;
    overflow: auto;
}

pre {
    background: #f6f6f6;
    border: 1px solid #ddd;
    padding: .125em;
}
a:link, a:visited {
    text-decoration: none;
}
a:link:hover, a:visited:hover {
    text-decoration: underline;
}