aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--doc/style.css18
1 files changed, 17 insertions, 1 deletions
diff --git a/doc/style.css b/doc/style.css
index 82239a2a..5cdf97ba 100644
--- a/doc/style.css
+++ b/doc/style.css
@@ -4,7 +4,21 @@ body {
}
#top {
- display: none;
+ background-color: #F3F3F3;
+ margin: 0;
+ padding: 0;
+ border-bottom: 1px solid #DDD;
+ margin-bottom: 1ex;
+ font-size: 180%;
+ font-weight: bold;
+}
+
+div.header {
+ display: none;
+}
+
+.tabs {
+ display: none;
}
h1 h2 h3 h4 h5 h6 {
@@ -553,4 +567,6 @@ div.header {
div.headertitle {
padding: 5px 5px 5px 10px;
+ font-size: 180%;
+ font-weight: bold;
}