web: Adjust sizes of monospace fonts.

120% is big enough, let's use this size everywhere.

diff --git a/web/para.css b/web/para.css
index 2207d6148371defedcfb23520482444ab0fddd7f..131493052e4486254b6296b4ba56737bd799f8b4 100644 (file)
--- a/web/para.css
+++ b/web/para.css
@@ -308,7 +308,7 @@ img.logo {
 
 div.page_header {
        padding: 8px;
-       font-size: 150%;
+       font-size: 120%;
        font-weight: bold;
        background-color: #151515;
 }
@@ -351,7 +351,7 @@ div.page_footer_text {
 div.page_body {
        padding: 8px;
        font-family: monospace;
-       font-size: 150%;
+       font-size: 120%;
 }
 
 a.title:hover {
@@ -367,6 +367,13 @@ div.title_text {
 
 div.log_body {
        padding: 8px 8px 8px 150px;
+       font-family: monospace;
+       font-size: 120%;
+}
+
+div.log {
+       font-family: monospace;
+       font-size: 120%;
 }
 
 span.age {