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

Remove some redundant checks

Browse source 
$sleep must already be an integer (due to type hints).

Change-Id: I468ea23cafd2706bdeb23676d8aab85daa09a599
This commit is contained in:
Bartosz Dziewoński 2024-08-12 22:58:49 +02:00
parent f8909a36da
commit 539946a92a
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
includes/Database.php
View file

@ -387,7 +387,7 @@ class Database {
public function migrateNamespace(
int $pageBatchSize, int $linterBatchSize, int $sleep
): int {
if ( gettype( $sleep ) !== 'integer' || $sleep < 0 ) {
if ( $sleep < 0 ) {
$sleep = 0;
}
@ -486,7 +486,7 @@ class Database {
public function migrateTemplateAndTagInfo(
int $batchSize, int $sleep
): int {
if ( gettype( $sleep ) !== 'integer' || $sleep < 0 ) {
if ( $sleep < 0 ) {
$sleep = 0;
}