mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/Linter
synced 2024-09-23 18:29:58 +00:00
df0f222fa3
Because linter_cat is the leftmost part of the linter_cat_page_position index, we don't need a separate one. Pointed out by jynus in T148866#2846381. Change-Id: I3b0e75b02762cc948baf8dbdfee67b611aa3b9c1
19 lines
751 B
SQL
19 lines
751 B
SQL
CREATE TABLE /*_*/linter (
|
|
-- primary key
|
|
linter_id int UNSIGNED PRIMARY KEY not null AUTO_INCREMENT,
|
|
-- page id
|
|
linter_page int UNSIGNED not null,
|
|
-- error category (see CategoryManager::$categoryIds)
|
|
linter_cat int UNSIGNED not null,
|
|
-- start and end positions of where the error is located
|
|
linter_start int UNSIGNED not null,
|
|
linter_end int UNSIGNED not null,
|
|
-- extra parameters about the error, JSON encoded
|
|
linter_params blob NOT NULL
|
|
) /*$wgDBTableOptions*/;
|
|
|
|
-- Query by page
|
|
CREATE INDEX /*i*/linter_page ON /*_*/linter (linter_page);
|
|
-- Unique index for lint errors, also covers linter_cat for query by category
|
|
CREATE UNIQUE INDEX /*i*/linter_cat_page_position ON /*_*/linter (linter_cat, linter_page, linter_start, linter_end);
|