+ 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;
+ }
+