From a3bfc1ac707025a56eee5aa780e64ecf5658d606 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 18 Jun 2024 12:39:59 +0200 Subject: [PATCH] fix: do not use currentScript attribute (#471) --- vscode-lean4/loogleview/index.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vscode-lean4/loogleview/index.ts b/vscode-lean4/loogleview/index.ts index 1580cb9d..8922a8e9 100644 --- a/vscode-lean4/loogleview/index.ts +++ b/vscode-lean4/loogleview/index.ts @@ -89,7 +89,7 @@ class LoogleView { private history: LoogleQueryHistory = new LoogleQueryHistory() private abbreviationConfig: AbbreviationConfig = JSON.parse( - document.currentScript!.getAttribute('abbreviation-config')!, + document.querySelector('script[data-id="loogleview-script"]')!.getAttribute('abbreviation-config')!, ) private rewriter: InputAbbreviationRewriter = new InputAbbreviationRewriter( this.abbreviationConfig,