-
- $ua = @$_SERVER['HTTP_USER_AGENT'];
- if( strcmp( $wgScript, $url ) && strpos( $ua, 'MSIE' ) !== false ) {
+
+ if( $url == '' ) {
+ # This will make the next check fail with a confusing error
+ # message, so we should mention it separately.
+ wfHttpError( 500, 'Internal Server Error',
+ "\$_SERVER['PHP_SELF'] is not set. Perhaps you're using CGI" .
+ " and haven't set cgi.fix_pathinfo = 1 in php.ini?" );
+ return;
+ }
+
+ if( strcmp( $wgScript, $url ) ) {