* Style tweak.

1 files changed, 7 insertions, 2 deletions

diff --git a/doc/manual/style.css b/doc/manual/style.css
index 6c8137ee3..e992a9a85 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;