Fix for r56924: don't do any mouseover/mouseout effects while the spinner is being...

diff --git a/includes/DefaultSettings.php b/includes/DefaultSettings.php
index d86f1cb..87edd1b 100644 (file)
--- a/includes/DefaultSettings.php
+++ b/includes/DefaultSettings.php
@@ -1606,7 +1606,7 @@ $wgCacheEpoch = '20030516000000';
  * to ensure that client-side caches do not keep obsolete copies of global
  * styles.
  */
-$wgStyleVersion = '241';
+$wgStyleVersion = '242';
 
 
 # Server-side caching:

diff --git a/skins/common/ajaxwatch.js b/skins/common/ajaxwatch.js
index 76d3734..2e1db0d 100644 (file)
--- a/skins/common/ajaxwatch.js
+++ b/skins/common/ajaxwatch.js
@@ -159,12 +159,15 @@ wgAjaxWatch.onLoad = function() {
          wgAjaxWatch.imgBasePath = el1.firstChild.firstChild.src
                                .replace( /\/vector\/images\/watch_(off|on).gif/, "" );
          el1.firstChild.onmouseover = function( e ) {
-           this.firstChild.src = wgAjaxWatch.imgBasePath
-                                       + "/vector/images/watch_over.gif";
+           if ( !wgAjaxWatch.inprogress )
+               this.firstChild.src = wgAjaxWatch.imgBasePath
+                       + "/vector/images/watch_over.gif";
          }
          el1.firstChild.onmouseout = function( e ) {
-           this.firstChild.src = wgAjaxWatch.imgBasePath
-                                       + "/vector/images/watch_" + ( wgAjaxWatch.watching ? "on.gif" : "off.gif");
+           if ( !wgAjaxWatch.inprogress )
+               this.firstChild.src = wgAjaxWatch.imgBasePath
+                       + "/vector/images/watch_" + ( wgAjaxWatch.watching ?
+                               "on.gif" : "off.gif" );
          }
        }
        } catch( e ) {