mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/Linter
synced 2024-11-23 23:44:17 +00:00
419610bcdb
Move location to two separate columns in the database: linter_start and linter_end. This allows us to have the database enforce the uniqueness of those fields, instead of just relying upon the PHP code to do so, which could be bypassed since we have multiple servers and concurrent processes. Change-Id: I3e67ce1b7cb3c93866a388ec3248af4cff2a81e0 |
||
---|---|---|
.. | ||
ApiQueryLintErrors.php | ||
ApiRecordLint.php | ||
CategoryManager.php | ||
Database.php | ||
Hooks.php | ||
LintError.php | ||
LintErrorsPager.php | ||
RecordLintJob.php | ||
SpecialLintErrors.php |