mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/Echo
synced 2024-12-12 07:55:53 +00:00
2862711ad2
Use foreach ( $array as $key => $value ) { instead of foreach ( array_keys( $array ) as $key ) { $value = $array[$key]; Change-Id: I3a75d3c7a2b41888998af37701ed9075380d286a |
||
---|---|---|
.. | ||
Api | ||
NotificationRequestJob.php | ||
NotificationServiceClient.php | ||
PushNotifier.php | ||
Subscription.php | ||
SubscriptionManager.php | ||
Utils.php |