fix: lint error.

lovettchris · lovettchris · commit f0c38063f689 · 2022-01-26T14:53:29.000-08:00
diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts
@@ -380,7 +380,7 @@ export class InfoProvider implements Disposable {
             editor.revealRange(selection, TextEditorRevealType.InCenterIfOutsideViewport);
             editor.selection = new Selection(selection.start, selection.end);
             // ensure the text document has the keyboard focus.
-            window.showTextDocument(editor.document, { viewColumn: editor.viewColumn, preserveFocus: false });
+            void window.showTextDocument(editor.document, { viewColumn: editor.viewColumn, preserveFocus: false });
         }
     }
 

Original file line number	Diff line number	Diff line change
`@@ -380,7 +380,7 @@ export class InfoProvider implements Disposable {`
`380`	`380`	`editor.revealRange(selection, TextEditorRevealType.InCenterIfOutsideViewport);`
`381`	`381`	`editor.selection = new Selection(selection.start, selection.end);`
`382`	`382`	`// ensure the text document has the keyboard focus.`
`383`		`- window.showTextDocument(editor.document, { viewColumn: editor.viewColumn, preserveFocus: false });`
	`383`	`+ void window.showTextDocument(editor.document, { viewColumn: editor.viewColumn, preserveFocus: false });`
`384`	`384`	`}`
`385`	`385`	`}`
`386`	`386`