fix: do not use currentScript attribute (#471)

leanprover · Jun 18, 2024 · a3bfc1a · a3bfc1a
1 parent de19e8a
commit a3bfc1a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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,