Even out padding

diff --git a/includes/DefaultSettings.php b/includes/DefaultSettings.php
index 6f48361..237a2e6 100644 (file)
--- a/includes/DefaultSettings.php
+++ b/includes/DefaultSettings.php
@@ -1436,7 +1436,7 @@ $wgCacheEpoch = '20030516000000';
  * to ensure that client-side caches don't keep obsolete copies of global
  * styles.
  */
-$wgStyleVersion = '186';
+$wgStyleVersion = '187';
 
 
 # Server-side caching:

diff --git a/skins/common/shared.css b/skins/common/shared.css
index 8dad1e1..58b28ce 100644 (file)
--- a/skins/common/shared.css
+++ b/skins/common/shared.css
@@ -152,10 +152,10 @@ div.searchdidyoumean {
 
 div.searchresults {
        border:1px solid darkblue;
-       padding-top: 5px;
-       padding-bottom: 5px;
-       padding-left: 15px;
-       padding-right: 15px;
+       padding-top: 10px;
+       padding-bottom: 10px;
+       padding-left: 10px;
+       padding-right: 10px;
 }
 
 /*