MediaWiki 1.19.5 E_USER_DEPRECATED error

MediaWiki v1.19.5 was released today with a number of vulnerabilities fixed. If you install this patch on a system with PHP 5.2.x, you will get a notice printed all over your wiki, stating something like this: "Use of undefined constant E_USER_DEPRECATED".

This happens because while MediaWiki v1.19 claims to support PHP 5.2.3+, patch v1.19.5 accidentally introduces a dependency on PHP 5.3.0+.

The fix

To fix this bug, simply open includes/GlobalFunctions.php in an editor, navigate to line 2219, and insert the following code:

if( !defined( 'E_USER_DEPRECATED' ) ) {
    define( 'E_USER_DEPRECATED', 16384 );
}

Explanation

MediaWiki v1.19.5 adds the constant E_USER_DEPRECATED into an expression on line 2219. This constant is only defined in PHP 5.3.0 and higher. But so is E_DEPRECATED, which was already present in that expression in v1.19.4 without causing a warning. Fortunately a fix for that is right here, next to the line: an explicit definition of E_DEPRECATED if it's not already defined. Clearly this was done for compatibility with PHP versions before 5.3.0, and clearly this was also supposed to have been done for E_USER_DEPRECATED.

This highlights the fact that this patch hasn't been tested on the earliest version of PHP claimed as supported. It really should have been.

P.S. I run OrbiterWiki, which is where this problem happened.