From 0ed9c9ed10b633aa7560c9c5873e9ade3ca20714 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 17 Oct 2024 19:08:01 +0200 Subject: [PATCH] fix: add another missing file to bundle --- vscode-lean4/.vscodeignore | 1 + 1 file changed, 1 insertion(+) diff --git a/vscode-lean4/.vscodeignore b/vscode-lean4/.vscodeignore index d69ec64c..1451c7b1 100644 --- a/vscode-lean4/.vscodeignore +++ b/vscode-lean4/.vscodeignore @@ -6,6 +6,7 @@ !dist/extension.js* !dist/webview.js* !dist/loogleview.js* +!dist/moogleview.js* !dist/abbreviationview.js* !dist/es-module-shims.js !dist/**/*.production.min.js