diff options
| -rw-r--r-- | doc/style.css | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/style.css b/doc/style.css index 5cdf97ba..c20312fc 100644 --- a/doc/style.css +++ b/doc/style.css @@ -6,19 +6,19 @@ body { #top { background-color: #F3F3F3; margin: 0; - padding: 0; + padding: 0; border-bottom: 1px solid #DDD; - margin-bottom: 1ex; - font-size: 180%; - font-weight: bold; + margin-bottom: 1ex; + font-size: 180%; + font-weight: bold; } div.header { - display: none; + display: none; } .tabs { - display: none; + display: none; } h1 h2 h3 h4 h5 h6 { @@ -567,6 +567,6 @@ div.header { div.headertitle { padding: 5px 5px 5px 10px; - font-size: 180%; - font-weight: bold; + font-size: 180%; + font-weight: bold; } |