From b5f0874cd96ee2a62aabc645b9626c2749cb6a01 Mon Sep 17 00:00:00 2001
From: manuel <manuel@mausz.at>
Date: Mon, 26 Mar 2012 12:54:45 +0200
Subject: initial pintos checkin

---
 doc/pintos.css | 76 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 76 insertions(+)
 create mode 100644 doc/pintos.css

(limited to 'doc/pintos.css')

diff --git a/doc/pintos.css b/doc/pintos.css
new file mode 100644
index 0000000..019a33d
--- /dev/null
+++ b/doc/pintos.css
@@ -0,0 +1,76 @@
+body {
+	background: white;
+	color: black;
+	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;
+	text-align: justify
+}
+body>p + p {
+	margin: .75em 0pt 0pt 0pt
+}
+H1 {
+	font-size: 150%;
+	margin-left: -1.33em
+}
+H2 {
+	font-size: 125%;
+	font-weight: bold;
+	margin-left: -.8em
+}
+H3 {
+	font-size: 100%;
+	font-weight: bold;
+	margin-left: -.5em }
+H4 {
+	font-size: 100%;
+	margin-left: 0em
+}
+H1, H2, H3, H4, H5, H6 {
+	font-family: sans-serif;
+	color: blue
+}
+H1, H2 {
+	text-decoration: underline
+}
+html {
+	margin: 0;
+	font-weight: lighter
+}
+tt, code {
+	font-family: sans-serif
+}
+b, strong {
+	font-weight: bold
+}
+
+a:link {
+	color: blue;
+        text-decoration: none;
+}
+a:visited {
+	color: gray;
+	text-decoration: none;
+}
+a:active {
+	color: black;
+	text-decoration: none;
+}
+a:hover {
+        text-decoration: underline
+}
+
+address {
+	font-size: 90%;
+	font-style: normal
+}
+
+HR {
+	display: none
+}
-- 
cgit v1.2.3