Adjust document style

1 files changed, 8 insertions, 0 deletions

diff --git a/doc.css b/doc.css
index d0a8e65..33054b5 100644
--- a/doc.css
+++ b/doc.css
@@ -33,6 +33,14 @@ h2
   margin: 1.6em 0 .6em -.8em;
 }
 
+h3
+{
+  font-weight: normal;
+  font-size: 1.3em;
+  line-height: 1.4em;
+  margin: 1.6em 0 .6em -.2em;
+}
+
 /* Title page */
 
 #titlepage {