Remove settings search @groupId filters - since group ids can now be extension guids, and nobody uses this anyway

This commit is contained in:
Rob Lourens
2018-01-19 10:37:28 -08:00
parent 9e34212e26
commit 5b7485c410

View File

@@ -106,17 +106,10 @@ export class LocalSearchProvider implements ISearchProvider {
}
private getGroupFilter(filter: string): IGroupFilter {
if (strings.startsWith(filter, '@')) {
const groupId = filter.replace(/^@/, '');
return (group: ISettingsGroup) => {
return group.id.toLowerCase() === groupId.toLowerCase();
};
} else {
const regex = strings.createRegExp(this._filter, false, { global: true });
return (group: ISettingsGroup) => {
return regex.test(group.title);
};
}
const regex = strings.createRegExp(this._filter, false, { global: true });
return (group: ISettingsGroup) => {
return regex.test(group.title);
};
}
}