New file, mkws-doc.css

Used only for HTML documentation generated from Markdown.

diff --git a/tools/htdocs/mkws-doc.css b/tools/htdocs/mkws-doc.css
new file mode 100644 (file)
index 0000000..6433806
--- /dev/null
+++ b/tools/htdocs/mkws-doc.css
@@ -0,0 +1,27 @@
+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;
+}