mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/Echo
synced 2024-12-18 02:40:50 +00:00
a10b0b07c8
Change-Id: I44144df7cf244eb867c1b261c10cc29b020f8409
29 lines
744 B
PHP
29 lines
744 B
PHP
<?php
|
|
|
|
namespace EchoPush;
|
|
|
|
use CentralIdLookup;
|
|
use MediaWiki\MediaWikiServices;
|
|
use MediaWiki\User\UserIdentity;
|
|
|
|
class Utils {
|
|
|
|
/**
|
|
* Attempt to get a unique ID for the specified user, accounting for installations both with
|
|
* and without CentralAuth: Return the user's central ID, if available. If there is no central
|
|
* user associated with the local user (i.e., centralIdFromLocalUser returns 0), fall back to
|
|
* returning the local user ID.
|
|
* @param UserIdentity $user
|
|
* @return int
|
|
*/
|
|
public static function getPushUserId( UserIdentity $user ): int {
|
|
return MediaWikiServices::getInstance()
|
|
->getCentralIdLookup()
|
|
->centralIdFromLocalUser(
|
|
$user,
|
|
CentralIdLookup::AUDIENCE_RAW
|
|
) ?: $user->getId();
|
|
}
|
|
|
|
}
|