From 6b5b60a31be6320936ab6ec693a3c918f3c8640b Mon Sep 17 00:00:00 2001 From: nmorozov Date: Tue, 12 Sep 2006 15:44:20 +0400 Subject: [PATCH] Smaller fonts for Arial-based styles, smaller margins Please enter the commit message for your changes. --- docs/site.css | 14 ++++++++------ 1 files changed, 8 insertions(+), 6 deletions(-) diff --git a/docs/site.css b/docs/site.css index 7aab0d9..ed68aec 100755 --- a/docs/site.css +++ b/docs/site.css @@ -98,6 +98,7 @@ pre { .class { font-weight: bold; + font-size: 10pt; font-family: Arial; border-top: none; border-right: none; @@ -113,6 +114,7 @@ pre { margin-top: 3pt; margin-bottom: 3pt; font-family: Arial, helvetica, sans-serif; + font-size: 10pt; } .backtotop { @@ -124,25 +126,25 @@ pre { color: red; font-weight: bolder; font-family: Arial, helvetica, sans-serif; + font-size: 10pt; } .notetext { - margin-left: 30pt; - margin-right: 30pt; + padding-left: 20pt; margin-top: 0pt; margin-bottom: 0pt; font-family: Arial, helvetica, sans-serif; - font-size: 11pt; + font-size: 10pt; } .example { font-weight: bolder; - padding: 4pt; font-family: Arial, helvetica, sans-serif; + font-size: 10pt; } .exampletext { - padding-left: 40pt; + margin-left: 40pt; } .TOCHeading { @@ -194,7 +196,7 @@ dl { } dd { - margin-left: 65pt; + margin-left: 30pt; margin-top: 5pt; margin-right: 20pt; margin-bottom: 5pt; -- 1.4.1