Merge pull request #1344 from glacambre/fix_help_completions

completions/Help.ts: Fix completions not being properly deselected
This commit is contained in:
Oliver Blanthorn 2019-02-10 11:50:56 +00:00 committed by GitHub
commit cd99fe78c5
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -30,6 +30,7 @@ export class HelpCompletionSource extends Completions.CompletionSourceFuse {
public async filter(exstr: string) {
this.lastExstr = exstr
this.completion = undefined
let [prefix, query] = this.splitOnPrefix(exstr)
let options = ""