# HG changeset patch
# User zas_
# Date 1226440242 0
# Node ID e0d275b9ebaa8df49c61bec8e291e5a401866ce7
# Parent  38238d1b2621ee396094b256652948b906cd4f43
Give a new style to menus.

diff -r 38238d1b2621 -r e0d275b9ebaa doc/style.css
--- a/doc/style.css	Tue Nov 11 21:49:33 2008 +0000
+++ b/doc/style.css	Tue Nov 11 21:50:42 2008 +0000
@@ -96,9 +96,25 @@
 }
 .menu_desc dt {
 	font-weight: bold;
-	padding-top: 0.3em;
+	padding: 0.1em;
+	border-left: 1px solid gray;
+	border-bottom: 1px solid gray;
+	display: inline;
+	vertical-align: top;
 }
 .menu_desc dd {
+	margin-top: 0.3em;
+	margin-bottom: 0.3em;
+	font-size: small;
+}
+
+.menu_desc dd dl {
+	margin-top: 0.7em;
+	margin-bottom: 0.7em;
+}
+
+.menu_desc dd dl dd {
+	font-size: small;
 }
 
 /* dialog descriptions */