search: Avoid duplicate search results from case sensitivity.

Previously, if you typed "channel: rome" you'd see a result for
both channel "rome" and a second one for "Rome". This commit
deduplicates that by comparing for duplicates without case
sensitivity.

Note that if you fully type "channel: rome" you'll see the
result with a lowercase R instead of uppercase. It would
be a bit involved to change this, so I'm leaving that as
something to address in the future.
This commit is contained in:
evykassirer 2024-07-18 11:57:47 -07:00 committed by Tim Abbott
parent cbe2677a2a
commit d23d8b8565
1 changed files with 2 additions and 2 deletions

View File

@ -853,8 +853,8 @@ class Attacher {
push(suggestion_line: SuggestionLine): void {
const search_string = suggestion_search_string(suggestion_line);
if (!this.prev.has(search_string)) {
this.prev.add(search_string);
if (!this.prev.has(search_string.toLowerCase())) {
this.prev.add(search_string.toLowerCase());
this.result.push(suggestion_line);
}
}