Updated to use Bochs 2.6.11

[pintos-anon] / doc / pintos.css

diff --git a/doc/pintos.css b/doc/pintos.css
index b00c2ce8432c9c12cc01fc051b1b7d56cde6f491..0af878f2f63d52ad36613b21ee1fdb1e7daaaa7d 100644 (file)
--- a/doc/pintos.css
+++ b/doc/pintos.css
@@ -1,11 +1,16 @@
 body {
        background: white;
        color: black;
-       padding: 0em 12em 0em 3em;
-       margin: 0
+       padding: 0em 1em 0em 3em;
+       margin: 0;
+       margin-left: auto;
+       margin-right: auto;
+       max-width: 8in;
+       text-align: justify
 }
 body>p {
-       margin: 0pt 0pt 0pt 0em
+       margin: 0pt 0pt 0pt 0em;
+       text-align: justify
 }
 body>p + p {
        margin: .75em 0pt 0pt 0pt
@@ -31,12 +36,19 @@ H1, H2, H3, H4, H5, H6 {
        font-family: sans-serif;
        color: blue
 }
+H1, H2 {
+       text-decoration: underline
+}
 html {
-       margin: 0
+       margin: 0;
+       font-weight: lighter
 }
-code {
+tt, code {
        font-family: sans-serif
 }
+b, strong {
+       font-weight: bold
+}
 
 a:link {
        color: blue;
@@ -54,75 +66,11 @@ a:hover {
         text-decoration: underline
 }
 
-div.menu {
-       margin: 0;
-       font-size: 80%;
-       font-weight: bold;
-       line-height: 1.1;
-       text-align: center;
-       position: absolute;
-       top: 2em;
-       left: auto;
-       width: 8.5em;
-       right: 2em;
-}
-div.menu p, span.menuitem {
-       display: block;
-       margin: 0;
-       padding: 0.3em 0.4em;
-       font-family: Arial, sans-serif;
-       background: #ddd;
-       border: thin outset #000;
-       color: #000;
-       text-indent: 0em;
-}
-IMG.menuimg {
-       width: 50%;
-       height: auto;
-       border-width: 0
-}
-
-div.menu a, div.menu em {
-       display: block;
-       margin: 0 0.5em
-}
-div.menu a, div.menu em {
-       border-top: 2px groove #000
-}
-div.menu a:first-child {
-       border-top: none
-}
-div.menu em {
-       color: #fff
-}
-
-div.menu a:link {
-       text-decoration: none;
-       color: blue
-}
-div.menu a:visited {
-       text-decoration: none;
-       color: gray
-}
-div.menu a:hover {
-       background: blue;
-       color: white
-}
-
-div.menu span.menugap + span.menuitem {
-       display: block;
-       margin-top: 1em
-}
-
-span.hide {
-       display: none
-}
-
-body>div.menu {
-       position: fixed
-}
-
 address {
        font-size: 90%;
        font-style: normal
 }
+
+HR { 
+       display: none
+}