Merge "Remove jquery.ui.spinner"

diff --combined resources/Resources.php
index 9638e9a,e958c26..591d54b
--- 1/resources/Resources.php
--- 2/resources/Resources.php
+++ b/resources/Resources.php
@@@ -591,18 -591,6 +591,6 @@@ return 
                ],
                'group' => 'jquery.ui',
        ],
-       'jquery.ui.spinner' => [
-               'scripts' => 'resources/lib/jquery.ui/jquery.ui.spinner.js',
-               'dependencies' => [
-                       'jquery.ui.core',
-                       'jquery.ui.widget',
-                       'jquery.ui.button',
-               ],
-               'skinStyles' => [
-                       'default' => 'resources/lib/jquery.ui/themes/smoothness/jquery.ui.spinner.css',
-               ],
-               'group' => 'jquery.ui',
-       ],
        'jquery.ui.tabs' => [
                'scripts' => 'resources/lib/jquery.ui/jquery.ui.tabs.js',
                'dependencies' => [
@@@ -1456,7 -1444,6 +1444,7 @@@
                'skinStyles' => [
                        'default' => 'resources/src/mediawiki.action/mediawiki.action.history.styles.css',
                ],
 +              'targets' => [ 'desktop', 'mobile' ],
        ],
        'mediawiki.action.view.dblClickEdit' => [
                'scripts' => 'resources/src/mediawiki.action/mediawiki.action.view.dblClickEdit.js',