#
#
# patch "texinfo.css"
#  from [b308324f50c748e6b2200e22e7be6637670d58da]
#    to [7f33c3a897d057b23d063e953e11fe3201e3712b]
#
============================================================
--- texinfo.css	b308324f50c748e6b2200e22e7be6637670d58da
+++ texinfo.css	7f33c3a897d057b23d063e953e11fe3201e3712b
@@ -214,6 +214,7 @@ dl dd dl {
 
 dl dd dl {
     font-size: 0.7692em;
+    margin-top: 1em;
 }
 
 dl dt + dd {