* MediaWiki version number
* @since 1.2
*/
-$wgVersion = '1.31.0-rc.0';
+$wgVersion = '1.31.1';
/**
* Name of the site. It must be changed in LocalSettings.php
* Even correct usage may cause failures with Unicode supplementary
* characters (those not in the Basic Multilingual Plane) unless MySQL
* has enhanced their Unicode support.
+ *
+ * @deprecated since 1.31
*/
$wgDBmysql5 = false;
'edit' => [
'ip' => [ 8, 60 ],
'newbie' => [ 8, 60 ],
+ 'user' => [ 90, 60 ],
],
// Page moves
'move' => [