diff -r 17d845dacff5 -r 0b0bb1608b37 web/common.css
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/web/common.css	Thu Jun 05 21:44:38 2008 -0400
@@ -0,0 +1,4 @@
+body { padding: 0 3em; }
+h1, h2, h3 { margin-left: -1em; }
+span.pname { font-family: monospace; }
+pre { margin-left: 2em; }