changeset 1135:e0d275b9ebaa

Give a new style to menus.
author zas_
date Tue, 11 Nov 2008 21:50:42 +0000
parents 38238d1b2621
children 7e902fefa7cd
files doc/style.css
diffstat 1 files changed, 17 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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 */