reduce border

diff --git a/doc/style.css b/doc/style.css
index bdd4bb4666faca9bbc74bb785f3c35778b2ed4a5..44e06ae4f67453fbc45d69fe88568d0385fab39e 100644 (file)
--- a/doc/style.css
+++ b/doc/style.css
@@ -236,7 +236,7 @@ div.recentchanges {
        margin-top: -1px;
        padding: 0ex 2ex;
        background: white;
-       border: 2px solid black;
+       border: 1px solid black;
        color: black !important;
 }