From b67e3a4102fd607f7d9133f74467b76deb0a652a Mon Sep 17 00:00:00 2001
From: Mark Lentczner <markl@glyphic.com>
Date: Fri, 13 Aug 2010 16:43:43 +0000
Subject: [PATCH] adjusted font sizes of auxilary pages per new scheme

---
 html/Ocean.std-theme/ocean.css | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/html/Ocean.std-theme/ocean.css b/html/Ocean.std-theme/ocean.css
index d7eac671b6..896aa8a21a 100644
--- a/html/Ocean.std-theme/ocean.css
+++ b/html/Ocean.std-theme/ocean.css
@@ -452,20 +452,20 @@ div.top .subs, div.top .doc {
 /* @group Auxillary Pages */
 
 #mini {
-  font-size: 75%;
+  font-size: 77%; /* 10pt */
   margin: 0 auto;
   padding: 0 1em;
 }
 
 #mini #module-header .caption {
-  font-size: 160%;
+  font-size: 130%;
 }
 
 #mini #interface h1,
 #mini #interface h2,
 #mini #interface h3,
 #mini #interface h4 {
-  font-size: 130%;
+  font-size: 100%;
   margin: 1em 0 0;
 }
 
@@ -474,10 +474,6 @@ div.top .subs, div.top .doc {
   margin: 0;
 }
 
-#mini #interface .src {
-  font-size: 120%;
-}
-
 #mini #module-list ul {
   list-style: none;
   margin: 0;
@@ -500,7 +496,7 @@ div.top .subs, div.top .doc {
 }
 
 #index .caption,
-#module-list .caption { font-size: 130%; }
+#module-list .caption { font-size: 131%; /* 17pt */ }
 
 #index table {
   margin-left: 2em;
@@ -510,7 +506,7 @@ div.top .subs, div.top .doc {
   font-weight: bold;
 }
 #index .alt {
-  font-size: 70%;
+  font-size: 77%; /* 10pt */
   font-style: italic;
   padding-left: 2em;
 }
-- 
GitLab