wikimedia/mediawiki-extensions-Gadgets
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/Gadgets synced 2024-11-27 16:50:00 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge "Tighten some type hints"

Browse source
This commit is contained in:
jenkins-bot 2022-01-20 02:03:10 +00:00 committed by Gerrit Code Review
parent 8ad07cc7a1 4e27ab0e01
commit 6fb18ae1fb
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
includes/Gadget.php
View file

@ -12,6 +12,8 @@
*/
use MediaWiki\MediaWikiServices;
use MediaWiki\Permissions\Authority;
use MediaWiki\User\UserIdentity;
/**
* Wrapper for one gadget.
@ -190,10 +192,10 @@ class Gadget {
/**
* Checks whether this gadget is enabled for given user
*
* @param User $user user to check against
* @param UserIdentity $user user to check against
* @return bool
*/
public function isEnabled( $user ) {
public function isEnabled( UserIdentity $user ) {
$userOptionsLookup = MediaWikiServices::getInstance()->getUserOptionsLookup();
return (bool)$userOptionsLookup->getOption( $user, "gadget-{$this->name}", $this->onByDefault );
}
@ -201,10 +203,10 @@ class Gadget {
/**
* Checks whether given user has permissions to use this gadget
*
* @param User $user The user to check against
* @param Authority $user The user to check against
* @return bool
*/
public function isAllowed( User $user ) {
public function isAllowed( Authority $user ) {
if ( count( $this->requiredRights ) ) {
return $user->isAllowedAll( ...$this->requiredRights );
}