css tweak

diff --git a/doc/docs.css b/doc/docs.css
index d65f5aff5ebdf6c651f3e601a1a6db1f4c0722d7..e78533cb834ec74d5afe509f2e9a2fdf83888081 100644 (file)
--- a/doc/docs.css
+++ b/doc/docs.css
@@ -148,6 +148,7 @@ h3 {
 
 .code {
        font-family: courier, "courier new", serif;
+       font-size:12px;
        background-color: #f0f0f0;      
        border: solid 1px #ccc;
        padding:2px 2px 2px 10px;