From a3fd53b9eb767c9b9f2c8f3824a1aea1c25544a6 Mon Sep 17 00:00:00 2001
From: Eelco Dolstra <e.dolstra@tudelft.nl>
Date: Wed, 4 Oct 2006 17:07:52 +0000
Subject: [PATCH] * Style tweak.

---
 doc/manual/style.css | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/doc/manual/style.css b/doc/manual/style.css
index 6c8137ee38..e992a9a85d 100644
--- a/doc/manual/style.css
+++ b/doc/manual/style.css
@@ -193,16 +193,21 @@ tt, code
     
 }
 
-div.variablelist dd p
+div.variablelist dd p, div.glosslist dd p
 {
     margin-top: 0em;
 }
 
-div.variablelist dd
+div.variablelist dd, div.glosslist dd
 {
     margin-left: 1.5em;
 }
 
+div.glosslist dt
+{
+    font-style: italic;
+}
+
 .default
 {
     font-style: italic;