Fix a small CSS glitch with deprecated blocks and Sphinx 1.2.

diff --git a/Doc/tools/sphinxext/static/basic.css b/Doc/tools/sphinxext/static/basic.css
index f05e35a314ddb3cf85418670efc89eb67cc621fe..89e4d7723d03bbad1b9ed927c76e79bf1c9800f8 100644 (file)
--- a/Doc/tools/sphinxext/static/basic.css
+++ b/Doc/tools/sphinxext/static/basic.css
@@ -337,7 +337,11 @@ dl.glossary dt {
 .deprecated {
     background-color: #ffe4e4;
     border: 1px solid #f66;
-    padding: 7px
+    padding: 7px;
+}
+
+div.deprecated p {
+    margin-bottom: 0;
 }
 
 .system-message {