Tone down the user margins

diff --git a/includes/DefaultSettings.php b/includes/DefaultSettings.php
index 2e6cebd..f8a9b5c 100644 (file)
--- a/includes/DefaultSettings.php
+++ b/includes/DefaultSettings.php
@@ -1343,7 +1343,7 @@ $wgCacheEpoch = '20030516000000';
  * to ensure that client-side caches don't keep obsolete copies of global
  * styles.
  */
-$wgStyleVersion = '131';
+$wgStyleVersion = '132';
 
 
 # Server-side caching:

diff --git a/skins/common/shared.css b/skins/common/shared.css
index fca3743..dba01a9 100644 (file)
--- a/skins/common/shared.css
+++ b/skins/common/shared.css
@@ -113,8 +113,8 @@ table.mw-userrights-groups * td,table.mw-userrights-groups * th {
 /* the auto-generated edit comments */
 .autocomment { color: gray; }
 #pagehistory .history-user {
-    margin-left: 1.4em;
-    margin-right: 0.4em;
+    margin-left: 0.4em;
+    margin-right: 0.2em;
 }
 #pagehistory span.minor { font-weight: bold; }
 #pagehistory li { border: 1px solid white; }