aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--html/Ocean.std-theme/ocean.css14
1 files changed, 5 insertions, 9 deletions
diff --git a/html/Ocean.std-theme/ocean.css b/html/Ocean.std-theme/ocean.css
index d7eac671..896aa8a2 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;
}