wikimedia/mediawiki-extensions-Echo
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/Echo synced 2024-09-23 18:30:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

Remove obsolete property name from @var docs

Browse source 
Change-Id: I72faac7f0f88b0e3c4f145aa1def0acae0398488
This commit is contained in:
Thiemo Kreuz 2020-08-10 12:53:14 +02:00
parent b2e643a47f
commit d046adfd99
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
includes/special/SpecialDisplayNotificationsConfiguration.php
View file

@ -18,7 +18,7 @@ class SpecialDisplayNotificationsConfiguration extends UnlistedSpecialPage {
/**
* Category names, mapping internal name to HTML-formatted name
*
* @var string[] $categoryNames
* @var string[]
*/
protected $categoryNames;
@ -27,14 +27,14 @@ class SpecialDisplayNotificationsConfiguration extends UnlistedSpecialPage {
/**
* Notification type names. Mapping HTML-formatted internal name to internal name
*
* @var string[] $notificationTypeNames
* @var string[]
*/
protected $notificationTypeNames;
/**
* Notify types, mapping internal name to HTML-formatted name
*
* @var string[] $notifyTypes
* @var string[]
*/
protected $notifyTypes;
@ -42,14 +42,14 @@ class SpecialDisplayNotificationsConfiguration extends UnlistedSpecialPage {
/**
* Category names, mapping HTML-formatted name to internal name
*
* @var string[] $flippedCategoryNames
* @var string[]
*/
protected $flippedCategoryNames;
/**
* Notify types, mapping HTML-formatted name to internal name
*
* @var string[] $flippedNotifyTypes
* @var string[]
*/
protected $flippedNotifyTypes;