From cbee7ec85bcf85b9fb9ae1df3fe6855fc2584330 Mon Sep 17 00:00:00 2001
From: Mark Lentczner <markl@glyphic.com>
Date: Wed, 18 Aug 2010 19:50:02 +0000
Subject: [PATCH] margin fiddling
---
html/Ocean.std-theme/ocean.css | 17 ++++++-----------
1 file changed, 6 insertions(+), 11 deletions(-)
diff --git a/html/Ocean.std-theme/ocean.css b/html/Ocean.std-theme/ocean.css
index e6d61d39b0..205b8e6e84 100644
--- a/html/Ocean.std-theme/ocean.css
+++ b/html/Ocean.std-theme/ocean.css
@@ -14,7 +14,9 @@ body {
text-align: left;
}
-p { margin: 0.5em 0; }
+p {
+ margin: 0.8em 0;
+}
ul { margin-left: 2em; }
@@ -83,7 +85,7 @@ dl.info {
.caption, h1, h2, h3, h4, h5, h6 {
font-weight: bold;
color: rgb(78,98,114);
- margin: 0.8em 0 0.5em;
+ margin: 0.8em 0 0.4em;
}
* + h1, * + h2, * + h3, * + h4, * + h5, * + h6 {
@@ -137,8 +139,7 @@ p.caption.expander {
pre {
padding: 0.25em;
-/* margin: 0.5em 5em 0.5em 3em; */
- margin: 0.5em 0 0.5em;
+ margin: 0.8em 0;
background: rgb(229,237,244);
overflow: auto;
border-bottom: 0.25em solid white;
@@ -155,12 +156,6 @@ pre {
.keyword { font-weight: normal; }
.def { font-weight: bold; }
-img.coll {
- width : 0.75em;
- height: 0.75em;
- margin: 0 0.5em 0 0;
-}
-
/* @end */
@@ -378,7 +373,7 @@ div#style-menu-holder {
margin: 0;
}
#interface td.doc p + p {
- margin-top: 0.5em;
+ margin-top: 0.8em;
}
#interface dt {
--
GitLab