Used only for HTML documentation generated from Markdown.
--- /dev/null
+body {
+ font-family: Times, "Times Roman", "Times New Roman";
+}
+
+h1, h2, h3 {
+ color: #666;
+ font-weight: bold;
+ font-family: Gill Sans, "Gillius ADF", Gillius, GilliusADF, Verdana, Sans-Serif;
+}
+
+h1 {
+ background: #eee;
+ padding: 0.2em;
+}
+
+p, ul, pre {
+ margin-left: 10em;
+}
+
+/*
+ * Works with the HTML emitted by pandoc. It would better if pandoc
+ * were to emit class names that we can use. But it doesn't.
+ */
+body p:last-of-type {
+ font-size: small;
+ text-align: right;
+}