X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fpintos.css;h=f904001d7a3d9188471ec59b2a360872db44102f;hb=1c71d8c6210ca64ccfa9d6056b7ea5b6a2c39802;hp=3dee90c4782ed4a7dbd1da9b78cab1e7f7ad8dd8;hpb=209f0b74c71b4eb5fed33ff4fa1271d3bc35b127;p=pintos-anon diff --git a/doc/pintos.css b/doc/pintos.css index 3dee90c..f904001 100644 --- a/doc/pintos.css +++ b/doc/pintos.css @@ -2,7 +2,11 @@ body { background: white; color: black; padding: 0em 1em 0em 3em; - margin: 0 + margin: 0; + margin-left: auto; + margin-right: auto; + max-width: 8in; + text-align: justify } body>p { margin: 0pt 0pt 0pt 0em; @@ -32,10 +36,14 @@ 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 }