* MediaWiki version number
* @since 1.2
*/
-$wgVersion = '1.31.0-rc.2';
+$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;