prevent page widening, but nicer.

diff --git a/website/local.css b/website/local.css
index 76dc4ccb644cbc70d902f9c644cd4eedd39ed453..f7a20060def5e74b710525dc267ce6824bb8a2c7 100644 (file)
--- a/website/local.css
+++ b/website/local.css
@@ -43,7 +43,7 @@ pre {
   border: 1px solid #aaa;
   padding: 3px 3px 3px 3px;
   margin-left: 2em;
-  overflow: scroll;
+  overflow: auto;
 }
 
 table.sitenav {