X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fpintos.css;h=0af878f2f63d52ad36613b21ee1fdb1e7daaaa7d;hb=3edcfedb8e62970f3293fa676b6691f8658c3c11;hp=b00c2ce8432c9c12cc01fc051b1b7d56cde6f491;hpb=ba48df561d04272b8cd819bf24c9cbde0f4bb085;p=pintos-anon

diff --git a/doc/pintos.css b/doc/pintos.css
index b00c2ce..0af878f 100644
--- 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
+}