X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fpintos.css;h=3dee90c4782ed4a7dbd1da9b78cab1e7f7ad8dd8;hb=5c9a85f896e888b26c6101e42d2b1072c7443e80;hp=b00c2ce8432c9c12cc01fc051b1b7d56cde6f491;hpb=806d0cd253880be54b78672581b9ff338bf2751f;p=pintos-anon

diff --git a/doc/pintos.css b/doc/pintos.css
index b00c2ce..3dee90c 100644
--- a/doc/pintos.css
+++ b/doc/pintos.css
@@ -1,11 +1,12 @@
 body {
 	background: white;
 	color: black;
-	padding: 0em 12em 0em 3em;
+	padding: 0em 1em 0em 3em;
 	margin: 0
 }
 body>p {
-	margin: 0pt 0pt 0pt 0em
+	margin: 0pt 0pt 0pt 0em;
+	text-align: justify
 }
 body>p + p {
 	margin: .75em 0pt 0pt 0pt
@@ -54,75 +55,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
+}