people: Fix bogus filter_people_by_search_terms type.

It actually returned Map<number, true>.  Set<number> is more
efficient.

Signed-off-by: Anders Kaseorg <anders@zulip.com>
This commit is contained in:
Anders Kaseorg
2024-05-03 13:55:58 -07:00
committed by Tim Abbott
parent fb7bad235d
commit 4032f9c0cb
2 changed files with 4 additions and 10 deletions

View File

@@ -343,10 +343,7 @@ function filter_user_ids(user_filter_text: string, user_ids: number[]): number[]
search_terms = search_terms.map((s) => s.trim());
const persons = user_ids.map((user_id) => people.get_by_user_id(user_id));
const user_id_dict = people.filter_people_by_search_terms(persons, search_terms);
return [...user_id_dict.keys()];
return [...people.filter_people_by_search_terms(persons, search_terms)];
}
function get_filtered_user_id_list(user_filter_text: string): number[] {